pm-06-chap03-程序規(guī)范及其正確性證明概述-免費(fèi)閱讀
【正文】 {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]} 這個(gè)證明梗概意味著下面各斷言依次為真： 1. P ? P1 2. {P1} i := i+1 {Q1} 3. Q1 ? P2 4. {P2} s :=s+b[i] {Q} 只要證明上面的 4個(gè)斷言為真， 就可以證明 {P} S {Q}為真。記為 [P] S [Q]。功能是把數(shù)組 b[m：n]各元素的值從小到大排列起來，使得最后的數(shù)組滿足 b[i] ≤ b[i+1]， i=m， … ,n1。 – 輸入?yún)?shù) ：在程序執(zhí)行前從外部獲得值，但在程序執(zhí)行中， 其值始終保持不變的變量 。 ? 它的意義： “ 若 S開始執(zhí)行時(shí) P為真，則 S的執(zhí)行必終止且終止時(shí) Q為真 ” 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 26 斷言與規(guī)范 (續(xù) ) ? 例：求商余程序 – {x1=0 and x20} – Y2:=x1。 6. 形式化程序規(guī)范描述語言簡介－ B語言簡介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 21 程序規(guī)范與程序 (續(xù) ) 6. Z語言、 VDM、 B形式化方法的比較 屬性 Z VDM B 基礎(chǔ) 謂詞演算 , 集合論 , 模式 偏函數(shù) , 集合論 最弱前置條件 , 集合論 開發(fā)階段 規(guī)范說明 規(guī)范說明 , 設(shè)計(jì) 規(guī)范說明 , 設(shè)計(jì) , 實(shí)現(xiàn) 形式 模式的符號表示 , 關(guān)系 前 /后置條件 , 函數(shù) 嚴(yán)格的編程語言 工具支持 在規(guī)格說明級 在規(guī)格說明級 BToolkit,AtchierB,所有開發(fā)階段 培訓(xùn)支持 圖書、課程 圖書 , 課程 實(shí)例研究、課程 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 22 內(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 23 斷言與規(guī)范 1. 斷言 – 斷言就是關(guān)于事物性質(zhì)的陳述 。 ? Ｂ 語言 是一種健全的 面向?qū)嶋H軟件過程 的 基于數(shù)學(xué)理論 的技術(shù) 。 ? VDM是一種 功能構(gòu)造性規(guī)格說明技術(shù) ，它通過 一階謂詞邏輯和已建立的抽象數(shù)據(jù)類型 來描述每個(gè)運(yùn)算或函數(shù)的功能。軟件系統(tǒng)的Ｚ模式規(guī)格說明可以按一定的層次結(jié)構(gòu)給出。有三種模式： – 自然語言： 不夠準(zhǔn)確，存在二義性，必須輔以數(shù)學(xué)語言。 – 所謂 “ 做什么 ” 是指對欲求解的問題的描述。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 4 程序規(guī)范與程序 (續(xù) ) 2. 程序 – 程序也是映射，是 輸入到計(jì)算的映射 ，即每一輸入都對應(yīng)一串計(jì)算步。但存在 過于規(guī)范 的問題。 ⑷ Ｚ語言難以由計(jì)算機(jī)直接處理。 ? 一個(gè) VDM規(guī)范有以下不同的塊組成： types type definitions values value definitions functions function definitions operations operation definitions state state name of state definition end 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 17 程序規(guī)范與程序 (續(xù) ) ? 缺點(diǎn)： ⑴ 由于 VDM對抽象數(shù)據(jù)類型預(yù)先定義了運(yùn)算，而某些用戶定義的類型在規(guī)格說明描述中無需這么多運(yùn)算，因而產(chǎn)生了 運(yùn)算冗余 。 –模塊化構(gòu)造 ：從規(guī)格說明到實(shí)現(xiàn)的模塊化構(gòu)造允許將規(guī)格說明和驗(yàn)證過程分解為多個(gè)子任務(wù)來進(jìn)行。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 25 斷言與規(guī)范 (續(xù) ) ? 程序斷言是對程序的性質(zhì)的陳述。 – {x1=x2*y1+y2 and 0=y2x2} 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 27 斷言與規(guī)范 (續(xù) ) ? 問題 ： – 如何構(gòu)造斷言使他們能準(zhǔn)確地反映不同位置上程序的性質(zhì)？ – 有了斷言，如何證明他們的正確性？ – 能否有準(zhǔn)則，可以從規(guī)范（ P， Q）構(gòu)造出程序 S，使 {P} S {Q}為真。這些變量不得在程序中出現(xiàn)，用以 u開頭的變量表示。 – 所謂一個(gè)狀態(tài)是滿足 P（或 Q）的，
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1