pm-06-chap03-程序規(guī)范及其正確性證明概述(文件)
【正文】 執(zhí)行時(shí)間、響應(yīng)周期等與時(shí)間有關(guān)性能指標(biāo)。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ì)之前，第一步必須明確 “ 做什么 ” 。 – PS是軟件工程的需求分析的結(jié)果。 – 描述一個(gè)復(fù)雜問題的輸入和輸出之間的關(guān)系是困難的，目前對(duì)規(guī)范語言的模式尚無定論。 – 數(shù)學(xué)語言： 用數(shù)學(xué)語言可以把輸入和輸出的映射描述為函數(shù)。 ? Ｚ語言的模式和模式演算： – 狀態(tài)模式 對(duì)目標(biāo)軟件系統(tǒng)的 結(jié)構(gòu)特征 進(jìn)行抽象描述； – 操作模式 對(duì)目標(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ù) ) ? Ｚ模式說明可以 組合成新的Ｚ模式 ，新的Ｚ模式繼承其成分模式的一切屬性和約束。 ⑵ 難以識(shí)別影響某一狀態(tài)模式的所有操作模式。初衷是為了描述 PL/1語言的語義。 ? 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ù)。 ? Ｂ 語言 是計(jì)算機(jī)輔助軟件工程中 Ｂ技術(shù)、方法和工具集的簡稱 。 ? Ｂ方法用一種簡單的 偽程序語言來描述需求模型 、說明接口，并進(jìn)行中間設(shè)計(jì)和實(shí)現(xiàn)； ? B語言就是 AMN（抽象機(jī)器符號(hào)）， AMN支持規(guī)格說明的類型檢測、動(dòng)態(tài)驗(yàn)證、數(shù)學(xué)證明等來確保設(shè)計(jì)過程的正確。 –成功的工業(yè)應(yīng)用 ： B語言和方法已在很多的工業(yè)領(lǐng)域得到成功應(yīng)用，包括實(shí)時(shí)、仿真、信息處理和工程等。 – 例 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）。 其中，（ P， Q）是程序 S的程序規(guī)范， S是一個(gè)程序（或語句） ? 斷言 {P} S {Q}稱為 S關(guān)于（ P， Q）的正確性斷言。 y1:=y1+1。如果是可變的，必要時(shí)對(duì)前者還需指明其變化方式。一般以 y開頭的變量，或不以 x和 u開頭的變量標(biāo)識(shí)。 ? 其規(guī)范 : – ({y1=u1∧ y2=u2}， {y1=u2∧ y2=u1}) 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 30 斷言與規(guī)范 (續(xù) ) 例 2：對(duì)數(shù)組 b[m： n]進(jìn)行排序的程序。作為某一個(gè)規(guī)范（ P， Q）的實(shí)現(xiàn)程序 S， S不得包含輔助變量， S也不得對(duì)輸入?yún)?shù)進(jìn)行任何形式的賦值，這些就是對(duì)規(guī)范（ P， Q）和斷言{P}S{Q}的語法規(guī)定。 ? 定義 2：對(duì)于滿足 P(ā)為真，且能夠使程序 S計(jì)算終止的每個(gè) ā，如果 Q(ā, P(ā))為真， 則稱程序 S對(duì)于 P和 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í)行，其中的
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1