Z规格说明的推理与验证

摘要：

Z规格说明具有非形式规约不可比拟的严谨性、清晰性.这种描述对于系统内对象的状态描述、行为描述是非常有用的原始参照物.但是,形式化描述不可避免的可能会含有错误或者是矛盾,这些问题在后期必定会导致前期的形式化设计不能付诸实践.因此,有必要做一些形式化的推理与验证来确保Z规约的实施.形式化推理是基于Z规格说明对一个操作模式求其前置条件,即求一个操作成功执行的必要条件,然后对比客观条件是否满足必要条件;形式化验证是一个操作模式求其后置条件,从集合的角度出发验证一个操作成功执行之后所导致的状态量变化是否与操作模式描述一致.

关键词：Z规格说明、推理、验证、形式化、条件

所属期刊栏目：32

分类号：TP393(计算技术、计算机技术)

资助基金：河北省高等学校高层次人才科学研究项目GCC2014010

在线出版日期：2017-01-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：12-16