pm-06-chap03-程序規(guī)范及其正確性證明概述(存儲版)
【正文】 若在此狀態(tài)下 P（或 Q）為真。 如果所有斷言 {Pi} Si {Qi}， i=1， 2， … ,n,為真，并且 每個(gè)蘊(yùn)涵： Qi ? Pi+1， i=1， 2， … ,n 成立， 就稱（ P1， Q1）， （ P2， Q2）， … , （ Pn， Qn）是{P}S{Q}的一個(gè)證明。運(yùn)行時(shí)間只允許幾分鐘； 10秒鐘是最適宜的運(yùn)行時(shí)間 – 要求：寫出實(shí)現(xiàn)方案；實(shí)現(xiàn) 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 41 小結(jié) ? 程序規(guī)范、規(guī)范的表示方法 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 – 完全正確性、部分正確性、終止性 ? 程序正確性證明的過程 – 證明 {P} S {Q}成立的過程 。 程序正確性概念 (續(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章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 37 程序的非形式化正確性證明簡介 ? 設(shè)（ P， Q）是一個(gè)規(guī)范， S是依照這個(gè)規(guī)范要求設(shè)計(jì)的程序，且是由語句 s1， s2， … ， sn組成的一個(gè)枚舉型程序（即其執(zhí)行等于組成它的各個(gè)語句的逐一順序的執(zhí)行，其中的每個(gè)語句都只有一個(gè)入口和一個(gè)出口，且沒有 GOTO語句）。作為某一個(gè)規(guī)范（ P， Q）的實(shí)現(xiàn)程序 S， S不得包含輔助變量， S也不得對輸入?yún)?shù)進(jìn)行任何形式的賦值，這些就是對規(guī)范（ P， Q）和斷言{P}S{Q}的語法規(guī)定。一般以 y開頭的變量，或不以 x和 u開頭的變量標(biāo)識。 y1:=y1+1。 – 例 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）。 ? Ｂ方法用一種簡單的 偽程序語言來描述需求模型 、說明接口，并進(jìn)行中間設(shè)計(jì)和實(shí)現(xiàn)； ? B語言就是 AMN（抽象機(jī)器符號）， AMN支持規(guī)格說明的類型檢測、動態(tài)驗(yàn)證、數(shù)學(xué)證明等來確保設(shè)計(jì)過程的正確。 ? 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é)概念和符號 來規(guī)定運(yùn)算或函數(shù)的功能； ? 可使軟件系統(tǒng)的功能描述在 抽象級 上進(jìn)行，完全擺脫了實(shí)現(xiàn)細(xì)節(jié)，這樣為軟件實(shí)現(xiàn)者提供了很大的靈活性； ? 這種形式化規(guī)格說明還為 程序正確性證明 提供了依據(jù)。 ⑵ 難以識別影響某一狀態(tài)模式的所有操作模式。 – 數(shù)學(xué)語言： 用數(shù)學(xué)語言可以把輸入和輸出的映射描述為函數(shù)。 – PS是軟件工程的需求分析的結(jié)果。 ? 這里的 PS僅指功能的描述，不包括諸如處理速度、執(zhí)行時(shí)間、響應(yīng)周期等與時(shí)間有關(guān)性能指標(biāo)。如 Hoare系統(tǒng)。 ? 模式例 : 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 // 在輸
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1