pm-06-chap03-程序規(guī)范及其正確性證明概述-資料下載頁
2025-08-04 10:35本頁面
【正文】 S對于 P和 Q是完全正確的。 記為 {P} S{Q} ? {P} S{Q} iff (? ā)(?p(ā) ? ((? S terminates) and ? Q(ā, P(ā))) ? [P] S [Q] iff (?ā)((?p(ā) and (? S terminates))?? Q(ā, P(ā)) 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 35 （ 1）關(guān)于部分正確性證明的方法 – Floyd 的不變式斷言法 – Manna的子目標(biāo)斷言法 – Hoare的公理化方法 （ 2）關(guān)于終止性證明的方法 – Floyd的良序集方法 – Knuth的計數(shù)器方法 – Manna等人的不動點方法 （ 3）關(guān)于完全正確性的證明方法 – Hoare的公理化方法（ Manna、 Pnueli） – Bustall的間發(fā)斷言法 – Dijkstra的弱謂詞轉(zhuǎn)換方法以及強驗證方法。 程序正確性概念 (續(xù) ) 主要的程序正確性證明方法 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 36 內(nèi)容－ Where we are？ ? 程序規(guī)范、規(guī)范的表示方法 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 ? 程序正確性證明的過程 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 37 程序的非形式化正確性證明簡介 ? 設(shè)（ P， Q）是一個規(guī)范， S是依照這個規(guī)范要求設(shè)計的程序，且是由語句 s1， s2， … ， sn組成的一個枚舉型程序（即其執(zhí)行等于組成它的各個語句的逐一順序的執(zhí)行，其中的每個語句都只有一個入口和一個出口，且沒有 GOTO語句）。令 P1,Q1,P2,Q2,… ,Pn,Qn是 2n個謂詞，且 P=P1，Q=Qn。 如果所有斷言 {Pi} Si {Qi}， i=1， 2， … ,n,為真，并且 每個蘊涵： Qi ? Pi+1， i=1， 2， … ,n 成立， 就稱（ P1， Q1）， （ P2， Q2）， … , （ Pn， Qn）是{P}S{Q}的一個證明。 例 1： 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 38 程序的非形式化正確性證明簡介 (續(xù) ) ? 例 1：令（ P， Q）為： P： {i≥0∧ s=b[0]+… +b[i]} Q： {i0 ∧ s=b[0]+… +b[i]} 令 S為： i := i+1 。 s :=s+b[i] 簡單證明如下： {P： i≥0∧ s=b[0]+… +b[i]} {P1： i+10∧ s=b[0]+… +b[i+11]} i := i+1 。 {Q1: i0∧ s=b[0]+… +b[i1]} {P2: i0∧ s+b[i]=b[0]+… +b[i1] +b[i]} s :=s+b[i] {Q: i0 ∧ s=b[0]+… +b[i]} 這個證明梗概意味著下面各斷言依次為真： 1. P ? P1 2. {P1} i := i+1 {Q1} 3. Q1 ? P2 4. {P2} s :=s+b[i] {Q} 只要證明上面的 4個斷言為真， 就可以證明 {P} S {Q}為真。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 39 思考練習(xí) 寫出下面問題的規(guī)范 : 1) 計算一個整數(shù)的絕對值； 2) 求兩個整數(shù)的最大值； 3) 求兩個非負整數(shù)的最大公約數(shù)； 4) 置 y等于數(shù)組 b[0:n1]中的最大值的位置； 5) 判定一個大于 1的整數(shù)是否素數(shù)； 6) 判斷數(shù)組 b[0:n1]是否已排序了； 7) 求數(shù)組 a[0:n1]與 b[0:n1]的內(nèi)積 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 40 作業(yè)： ? 1. 編程 – 輸入：輸入一個文件，至多包含 n個正整數(shù)，每個正整數(shù)都不大于 n，例如， n＝ 10**輸入時某個整數(shù)出現(xiàn)兩次，就會產(chǎn)生一個致命的錯誤。這些整數(shù)與其他任何整數(shù)都不關(guān)聯(lián) – 輸出：以增序形式輸出經(jīng)過排序的整數(shù)列表 – 約束：至多只有 1MB的可用內(nèi)存；但是磁盤空間足夠。運行時間只允許幾分鐘； 10秒鐘是最適宜的運行時間 – 要求：寫出實現(xiàn)方案；實現(xiàn) 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機軟件所 程序設(shè)計方法學(xué) All Rights Reserved 41 小結(jié) ? 程序規(guī)范、規(guī)范的表示方法 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 – 完全正確性、部分正確性、終止性 ? 程序正確性證明的過程 – 證明 {P} S {Q}成立的過程
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1