结构化和面向对象的软件形式方法研究

经过项目研究，在理论和方法实现上均取得成果：对面向对象的Z进行了研究，设计了面向对象的语言OOZS，并在实现原理、类型检查、正确性判定和精化等方面取得成果；对结构化方法、面向对象方法和形式方法进行了比较，建立了一种称为结构化面向对象的形式方法的软件开发方法；定义了支持该方法的规格说明语言SOZL；并给出了从SOZL到代码的求精方法；在规格说明推理方面提出了策略模式语言；给出了Z规格说明定理的证明方法。对Z方法的应用进行了研究；实现了OOZS与可视化SOZL两个实验系统和一个标准Z规格说明语言的集成化支持系统Z User Studio。研究成果促进了软件形式方法的应用，可提高软件的可靠性和软件开发的效率。