【正文】 內(nèi)存；但是磁盤空間足夠。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 31 斷言與規(guī)范 (續(xù) ) ? 程序規(guī)范總結(jié)： – 在做程序規(guī)范時(shí)，必須區(qū)分三種變量： 輸入變量、輸出變量、輔助變量 。 – {0=y2 and 0x2 and x1=x2*y1+y2} – While y2=x2 do – begin {0=y2 and 0x2＝ y2 and x1=x2*y1+y2} – y2 :=y2x2。 ? Ｂ方法的指導(dǎo)性原則：分層軟件的 逐步構(gòu)造伴隨著逐步的驗(yàn)證和校驗(yàn) ； 6. 形式化程序規(guī)范描述語言簡介－ B語言簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 19 程序規(guī)范與程序 (續(xù) ) ? Ｂ工具盒包括有大量的工具，所有的工具 集成在一個(gè)基于窗口 的軟件開發(fā)環(huán)境中，因而支持運(yùn)用Ｂ方法開發(fā)軟件的整個(gè)軟件過程； ? Ｂ工具 支持軟件的逐步構(gòu)造 ，其中的驗(yàn)證過程可用靜態(tài)分析，動(dòng)態(tài)分析采用模擬技術(shù)，正確性證明則使用集成的定理證明器。 ? 模式例 : 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 11 程序規(guī)范與程序 (續(xù) ) ? 模式例 1: [Student] // 引入基本類型 student StudentSys //模式名 Enrolled,tested: P Student // 聲明部分 , 學(xué)生的密集類型 enrolled ≤size // 斷言部分，合取關(guān)系 tested ? enrolled 等價(jià)于： //水平方式 StudentSys=[enrolled,tested: P Student | enrolled ≤size ? tested ? enrolled ] 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 4 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 12 程序規(guī)范與程序 (續(xù) ) ? 模式例 2: EnrollStudent ?StudentSys // = Studentsys ? StudentSys’的簡寫 name?: Student // 在輸入變量后加？ name? ? enrolled // 在輸出變量后加！ enrolled size // 帶有后綴‘的變量表示操作后的變量 enrolled’ = enrolled ∪ {name?} tested’= tested 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 5 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 13 程序規(guī)范與程序 (續(xù) ) ? 缺點(diǎn) : ⑴ Ｚ語言對(duì)大型系統(tǒng)的模塊化能力不足。 ? 這里的 PS僅指功能的描述，不包括諸如處理速度、執(zhí)行時(shí)間、響應(yīng)周期等與時(shí)間有關(guān)性能指標(biāo)。 – 數(shù)學(xué)語言： 用數(shù)學(xué)語言可以把輸入和輸出的映射描述為函數(shù)。 ? 1996年 ISO制訂了 VDM的國際標(biāo)準(zhǔn)化版本 VDMSL 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 15 程序規(guī)范與程序 (續(xù) ) ? VDM技術(shù)的基本思想： – 運(yùn)用 抽象數(shù)據(jù)類型、數(shù)學(xué)概念和符號(hào) 來規(guī)定運(yùn)算或函數(shù)的功能； ? 可使軟件系統(tǒng)的功能描述在 抽象級(jí) 上進(jìn)行，完全擺脫了實(shí)現(xiàn)細(xì)節(jié)，這樣為軟件實(shí)現(xiàn)者提供了很大的靈活性； ? 這種形式化規(guī)格說明還為 程序正確性證明 提供了依據(jù)。 – 例 1：寫一個(gè)計(jì)算商和余數(shù)的程序 ?程序規(guī)范： “ 設(shè)被除數(shù) x1是個(gè)非負(fù)整數(shù)，除數(shù) x2是個(gè)正整數(shù)，計(jì)算 x1除以 x2的商 y1和余數(shù) y2” ?又描述為： “ 初始條件： {x1=0 AND x20}, 計(jì)算滿足 {x1=x2*y1+y2 and 0=y2x2}的整數(shù) y1和 y2” 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 24 斷言與規(guī)范 (續(xù) ) 一般地，一個(gè)程序規(guī)范可表示為由兩個(gè)謂詞構(gòu)成的二元組（ P， Q）。一般以 y開頭的變量，或不以 x和 u開頭的變量標(biāo)識(shí)。 程序正確性概念 (續(xù) ) 主要的程序正確性證明方法 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 36 內(nèi)容－ Where we are？ ? 程序規(guī)范、規(guī)范的表示方法 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 ? 程序正確性證明的過程 第 3章