有限构模器的扩展及其在形式化方法中的应用

• 作者: 张健
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 形式规约 一阶谓词逻辑 有限模型构造 存在量词 传递闭包
• 年，卷（期）: 2000,（2）
• 所属期刊栏目: 短文
• 页码范围: 190-194
• 页数: 5页
• 分类号: TP18
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2000.02.012

摘要

规约在软件开发和验证中占有重要地位.对于以一阶逻辑为基础的规约,可以利用有限模型构造技术对其执行并测试.文中研究规约中某些特性的处理,包括存在量词以及二元关系的传递闭包.对已有的一个构模工具进行扩充,发现了文献中的若干错误.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张健	中国科学院软件研究所计算机科学开放研究实验室	272	3714	30.0	51.0