【基於COOZ的精化演算支撑工具的设计与实现】杨朝晖.pdf
学 号:论文答辩日期:221年6月6日 都目梁 指导教师:(签字)
基于COOZ的精化演算支撑工具的设计与实现 摘要 学基础,形式化规约可以进行形式确认、验证和精化,有利于实现软件自动 化。形式化方法与面向对象技术相结合的软件开发方法是软件工程的一大发 展方向。对乙进行面向对象扩充的COOZ可以精确描述大型软件系统的规 约,但不能由此直接得到可执行代码。精化演算是一种数学表示法和若干规 则的集合,用于从程序规约推导出命令式程序,是从规药到代码的转换过程.精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精 化的程序开发方法比对已有程序进行验证以保证程序正确性的方法史有效.精化过程可表示为分层结构。精化过程中产生大册要证明的定理。
基于COOZ的精化演算支撑工具的设计与实现 誉目 摘要,第一章绪 论:1问题的由来1形式化方法与面向对象技术的结合Z语言的面向对象扩充1国内外研究现状 1本文研究工作及组织第二章COOZ及其支撑环境简介.2引言2 Cooz(Complete Object-0rientedZ)简介2C0OZ的设计思想2在Z中引入对象类型.2模块机制2实时和历史约束.2对Z中模式的改进.2.