【一个COOZ精化工具的设计与实现】庞军.pdf
论文答辨日期:2000年3月30日 都周梁 指导教师:2(签字)
一个COOZ精化工具的设计和实现 摘 要 COOZ的优势在于精确描述大型程序的规约,COOZ本身的结构并 不支持精化演算,需要用证明的方法进行程序精化。这限制了COOZ 的应用能力,使COOZ难以作为完整的方法应用于软件的开发。将精 化演算引I入COOZ,弥补了COOZ在设计和实现阶段的不足,同时也 消除了规约与实现之间在构造和表示法上的分离,使程序开发可以在一个完整的框架下平滑进行。在这一框架下,可以采用COOZ的面向对 象形式规约技术描述软件的规约,然后采用精化演算的方法逐步精化到 程序代码.我们通过对现有精化工具的研究,提出一个可行的工具设计 方案和实现策略。
一个COOZ精化工具的设计和实现 目 帐 摘 要 ABSTRACT.ⅡI 目录 I 绪 论 1′1 问题的由来 1 意义 国内外研究现状 本文研究工作及组织 研究目标和内容 1 本文的组织.COOZ及其支撑环境的研究 2 COOZ(COMPLETE OBJECT-ORIENTED Z) COOZ的设计思想 2 对象类型 模块机制 实时和历史约束 对乙中模式的改进 2 支撑环境COOZ-TOOLS系统精化演算及其机器辅助技术 3 精化演算.