Z的面向对象扩充和程序转换系统的研究

本项研究集各家所长，对Z进行了面向对象扩充，使其能充分支持各种面向对象机制，并将其与面向对象软件开发过程相衔接。对COOZ的精化进行了理论研究，提出了子类型继承及推理规则。对面向对象精化演算进行了初步研究，提出一种类精化的方法。将面向对象Z规约与精化演算结合起来，建立一种逐步精化的面向对象形式化开发方法。研究中引入时段演算描述对象的实时和历史约束，使得COOZ适宜于描述实时和并发系统的形式规约，进一步发展了面向对象技术和形式化方法的集成技术，为开发高安全和高可靠软件提供了有效的方法。此外我们还设计和实现支持该Z面向对象扩充版本及其程序精化转换的实验性方案和系统。