結構化和面向對象的軟體形式方法研究

《結構化和面向對象的軟體形式方法研究》是依託上海大學，由繆淮扣擔任項目負責人的面上項目。

基本介紹

• 中文名：結構化和面向對象的軟體形式方法研究
• 項目類別：面上項目
• 項目負責人：繆淮扣
• 依託單位：上海大學
• 負責人職稱：教授
• 申請代碼：F0203
• 研究期限：1998-01-01 至 2000-12-31
• 批准號：69773038
• 支持經費：11（萬元）

中文摘要

經過項目研究，在理論和方法實現上均取得成果：對面向對象的Z進行了研究，設計了面向對象的語言OOZS，並在實現原理、類型檢查、正確性判定和精化等方面取得成果；對結構化方法、面向對象方法和形式方法進行了比較，建立了一種稱為結構化面向對象的形式方法的軟體開發方法；定義了支持該方法的規格說明語言SOZL；並給出了從SOZL到代碼的求精方法；在規格說明推理方面提出了策略模式語言；給出了Z規格說明定理的證明方法。對Z方法的套用進行了研究；實現了OOZS與可視化SOZL兩個實驗系統和一個標準Z規格說明語言的集成化支持系統Z User Studio。研究成果促進了軟體形式方法的套用，可提高軟體的可靠性和軟體開發的效率。