| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 有限构模器的扩展及其在形式化方法中的应用 |
| 作者 | 张 健 |
| 作者单位 | (中国科学院软件研究所计算机科学开放研究实验室 北京 100080) |
| 发表年份 | 2000 |
| 发表月份 | 2期 （页码：190—194) |
| 文章摘要 | 规约在软件开发和验证中占有重要地位.对于以一阶逻辑为基础的规约,可以利用有限模型构造技术对其执行并测试.文中研究规约中某些特性的处理,包括存在量词以及二元关系的传递闭包.对已有的一个构模工具进行扩充,发现了文献中的若干错误. 关键词 形式规约,一阶谓词逻辑,有限模型构造,存在量词,传递闭包 中图法分类号:TP18 |