摘要
规约在软件开发和验证中占有重要地位 .对于以一阶逻辑为基础的规约 ,可以利用有限模型构造技术对其执行并测试 .文中研究规约中某些特性的处理 ,包括存在量词以及二元关系的传递闭包 .对已有的一个构模工具进行扩充 。
Specifications play an important role in software development and verification. Logic based specifications can be executed and tested by finite model generation techniques. In this paper, some features of specifications are studied,including existential quantifiers and transitive closures of binary relations. An existing model generator is extended, and a few mistakes in the literature are identified.
出处
《计算机学报》
EI
CSCD
北大核心
2000年第2期190-194,共5页
Chinese Journal of Computers
基金
国家自然科学基金!( 6970 3 0 14 )
国家重点基础研究发展规划 (九七三 )( G19980 3 0 60 0 )
关键词
形式规约
软件开发
形式化方法
有限构模器
formal specifications, first order predicate logic, finite model construction, existential quantifiers, transitive closure