pm-06-chap03-程序規(guī)范及其正確性證明概述-全文預(yù)覽
【正文】 每個(gè)語(yǔ)句都只有一個(gè)入口和一個(gè)出口，且沒(méi)有 GOTO語(yǔ)句）。 s :=s+b[i] 簡(jiǎn)單證明如下： {P： i≥0∧ s=b[0]+… +b[i]} {P1： i+10∧ s=b[0]+… +b[i+11]} i := i+1 。運(yùn)行時(shí)間只允許幾分鐘； 10秒鐘是最適宜的運(yùn)行時(shí)間 – 要求：寫(xiě)出實(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} ? 程序正確性的概念 – 完全正確性、部分正確性、終止性 ? 程序正確性證明的過(guò)程 – 證明 {P} S {Q}成立的過(guò)程 。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 39 思考練習(xí) 寫(xiě)出下面問(wèn)題的規(guī)范 : 1) 計(jì)算一個(gè)整數(shù)的絕對(duì)值； 2) 求兩個(gè)整數(shù)的最大值； 3) 求兩個(gè)非負(fù)整數(shù)的最大公約數(shù)； 4) 置 y等于數(shù)組 b[0:n1]中的最大值的位置； 5) 判定一個(gè)大于 1的整數(shù)是否素?cái)?shù)； 6) 判斷數(shù)組 b[0:n1]是否已排序了； 7) 求數(shù)組 a[0:n1]與 b[0:n1]的內(nèi)積 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 40 作業(yè)： ? 1. 編程 – 輸入：輸入一個(gè)文件，至多包含 n個(gè)正整數(shù)，每個(gè)正整數(shù)都不大于 n，例如， n＝ 10**輸入時(shí)某個(gè)整數(shù)出現(xiàn)兩次，就會(huì)產(chǎn)生一個(gè)致命的錯(cuò)誤。 如果所有斷言 {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è)證明。 ? [P] S [Q] iff (?ā)((?p(ā) and (? S terminates))? ? Q(ā, P(ā)) 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 34 程序正確性概念 (續(xù) ) ? 定義 3：對(duì)于滿足 P(ā)為真的每個(gè) ā ，如果程序S能夠計(jì)算終止，且 Q(ā, P(ā))為真， 則稱程序S對(duì)于 P和 Q是完全正確的。 – 所謂一個(gè)狀態(tài)是滿足 P（或 Q）的，若在此狀態(tài)下 P（或 Q）為真。 ? 規(guī)范： – P： {m ≤n ∧ b[m:n]=u[m:n]} – Q： {m ≤n ∧ perm(b[m:n],u[m:n]) ∧ (?i: m ≤ i n : b[i] ≤b[i+1])} 其中， u[m:n]代表 b的任意可能初值； perm(b[m:n],u[m:n]) 是一個(gè)常謂詞，表示 b是 u的一個(gè)置換。這些變量不得在程序中出現(xiàn)，用以 u開(kāi)頭的變量表示。一般用以 x開(kāi)頭的標(biāo)識(shí)符表示。 – {x1=x2*y1+y2 and 0=y2x2} 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 27 斷言與規(guī)范 (續(xù) ) ? 問(wèn)題 ： – 如何構(gòu)造斷言使他們能準(zhǔn)確地反映不同位置上程序的性質(zhì)？ – 有了斷言，如何證明他們的正確性？ – 能否有準(zhǔn)則，可以從規(guī)范（ P， Q）構(gòu)造出程序 S，使 {P} S {Q}為真。 y1:=0。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 25 斷言與規(guī)范 (續(xù) ) ? 程序斷言是對(duì)程序的性質(zhì)的陳述。這個(gè)陳述可真可假。 –模塊化構(gòu)造 ：從規(guī)格說(shuō)明到實(shí)現(xiàn)的模塊化構(gòu)造允許將規(guī)格說(shuō)明和驗(yàn)證過(guò)程分解為多個(gè)子任務(wù)來(lái)進(jìn)行。 ? Ｂ方法所用的符號(hào)和方法支持大部分的軟件過(guò)程： 需求分析、規(guī)格說(shuō)明、軟件設(shè)計(jì)、實(shí)現(xiàn)和維護(hù) 。 ? 一個(gè) VDM規(guī)范有以下不同的塊組成： types type definitions values value definitions functions function definitions operations operation definitions state state name of state definition end 6. 形式化程序規(guī)范描述語(yǔ)言簡(jiǎn)介－ VDM簡(jiǎn)介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 17 程序規(guī)范與程序 (續(xù) ) ? 缺點(diǎn)： ⑴ 由于 VDM對(duì)抽象數(shù)據(jù)類型預(yù)先定義了運(yùn)算，而某些用戶定義的類型在規(guī)格說(shuō)明描述中無(wú)需這么多運(yùn)算，因而產(chǎn)生了 運(yùn)算冗余 。 ? 這種方法在 90年代初在歐美許多研究機(jī)構(gòu)或大學(xué)得到了廣泛的應(yīng)用。 ⑷ Ｚ語(yǔ)言難以由計(jì)算機(jī)直接處理。 ? Ｚ規(guī)格說(shuō)明由一系列模式組成，每個(gè)模式定
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1