【正文】 M目前還 未能建立一整套描述機(jī)制 ，將一個(gè)大型系統(tǒng)分解為許多運(yùn)算而描述出這些運(yùn)算之間的關(guān)系 ⑶ VDM形式規(guī)格說明 過于形式化 不容易理解 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 4 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 18 程序規(guī)范與程序 (續(xù) ) ? B方法是 20世紀(jì) 80年代初中期由 BP研究中心的 MATRA和 GE Alsthom研究小組開發(fā)的。 – 缺少商品化的工具支持等到諸多原因 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 6 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 14 程序規(guī)范與程序 (續(xù) ) ? VDM（ Vienna Development Method）是在 1969年為開發(fā) PL/1語言時(shí)，由 IBM公司維也納實(shí)驗(yàn)室 的研究小組提出的。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 6 程序規(guī)范與程序 (續(xù) ) 5. 一個(gè)合適的程序規(guī)范語言應(yīng)滿足的基本條件 : – 應(yīng)當(dāng)為描述者和使用者所直接理解； – 應(yīng)當(dāng)有嚴(yán)格的數(shù)學(xué)語義 – 應(yīng)當(dāng)與形式方法的構(gòu)造理論和程序設(shè)計(jì)語言協(xié)調(diào) – 應(yīng)當(dāng)有較強(qiáng)的表達(dá)能力和通用性 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 7 程序規(guī)范與程序 (續(xù) ) ? Z語言 ? VDM ? B方法 ? 三者的比較 6. 形式化程序規(guī)范描述語言簡介 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 8 程序規(guī)范與程序 (續(xù) ) ? Z語言是一種基于 集合論和一階謂詞邏輯 的形式化語言； ? Z語言支持軟件的 形式化規(guī)范描述，規(guī)范的推理和求精 ； ? 是迄今為止應(yīng)用最廣泛的形式語言之一； ? Z是在 Jean Raymond Abrial等的開創(chuàng)性工作下，由英國牛津大學(xué)的程序設(shè)計(jì)研究小組（ PRG， Programming Research Group），于 20世紀(jì) 80年代初開發(fā)； ? PRG與 IBM的 Hursley實(shí)驗(yàn)室合作， 將 Z語言用于 IBM的客戶信息控制系統(tǒng)的開發(fā) ，使得最終的 產(chǎn)品質(zhì)量 得到了全面的的提高，所測出的錯(cuò)誤數(shù)量大大減少，并且整體開發(fā)費(fèi)用 降低了 9％ ； ? 在 ISO指導(dǎo)下的國際標(biāo)準(zhǔn)化 Z工作于 2022年完成 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 9 程序規(guī)范與程序 (續(xù) ) ? 提供了一種稱為 模式（ Schema）的結(jié)構(gòu) ，它是Z的基本描述單位，以此來描述一個(gè)規(guī)范說明的狀態(tài)空間（靜態(tài)性質(zhì)）和操作（動(dòng)態(tài)行為） 。 3. 程序規(guī)范與程序的關(guān)系 – 給出規(guī)范后，程序開發(fā)就是建立一個(gè)程序，使得計(jì)算剛好能實(shí)現(xiàn)規(guī)范的映射； – 程序驗(yàn)證是 證明程序正確地實(shí)現(xiàn)了規(guī)范 ，即證明規(guī)范和已有程序之間的一致性 規(guī)范 程序 輸入 輸出 映射 輸入 計(jì)算 映射 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 5 程序規(guī)范與程序 (續(xù) ) 4. 程序規(guī)范的描述 規(guī)范語言 – 規(guī)范必須用語言描述，該語言稱為規(guī)范語言。1 第 3章 程序規(guī)范及其正確性證明概述 鮑玉斌 東北大學(xué)信息學(xué)院計(jì)算機(jī)軟件與理論研究所 August 20, 2022 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 2 內(nèi)容－ Where we are？ ? 程序規(guī)范、規(guī)范的描述 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 ? 程序正確性證明的過程 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 3 程序規(guī)范與程序 1. 程序規(guī)范： – 程序設(shè)計(jì)之前，第一步必須明確 “ 做什么 ” 。 – 描述一個(gè)復(fù)雜問題的輸入和輸出之間的關(guān)系是困難的，目前對規(guī)范語言的模式尚無定論。 ? Ｚ語言的模式和模式演算： – 狀態(tài)模式 對目標(biāo)軟件系統(tǒng)的 結(jié)構(gòu)特征 進(jìn)行抽象描述； – 操作模式 對目標(biāo)軟件系統(tǒng)的 行為特征 進(jìn)行抽象描述； – 通過 模式演算 ，無論多么大型系統(tǒng)的規(guī)格說明都可以通過一個(gè)個(gè)小的部分來構(gòu)成； 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 2 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 10 程序規(guī)范與程序 (續(xù) ) ? Ｚ模式說明可以 組合成新的Ｚ模式 ，新的Ｚ模式繼承其成分模式的一切屬性和約束。初衷是為了描述 PL/1語言的語義。 ? Ｂ 語