pm-06-chap03-程序規(guī)范及其正確性證明概述(編輯修改稿)
2025-08-31 10:35 本頁面
【文章內(nèi)容簡介】 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 18 程序規(guī)范與程序 (續(xù) ) ? B方法是 20世紀 80年代初中期由 BP研究中心的 MATRA和 GE Alsthom研究小組開發(fā)的。 ? Ｂ 語言 是計算機輔助軟件工程中 Ｂ技術、方法和工具集的簡稱 。 ? Ｂ 語言 是一種健全的 面向?qū)嶋H軟件過程 的 基于數(shù)學理論 的技術 。 ? Ｂ方法所用的符號和方法支持大部分的軟件過程： 需求分析、規(guī)格說明、軟件設計、實現(xiàn)和維護 。 ? Ｂ方法的指導性原則：分層軟件的 逐步構(gòu)造伴隨著逐步的驗證和校驗 ； 6. 形式化程序規(guī)范描述語言簡介－ B語言簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 19 程序規(guī)范與程序 (續(xù) ) ? Ｂ工具盒包括有大量的工具，所有的工具 集成在一個基于窗口 的軟件開發(fā)環(huán)境中，因而支持運用Ｂ方法開發(fā)軟件的整個軟件過程； ? Ｂ工具 支持軟件的逐步構(gòu)造 ，其中的驗證過程可用靜態(tài)分析，動態(tài)分析采用模擬技術，正確性證明則使用集成的定理證明器。 ? Ｂ方法用一種簡單的 偽程序語言來描述需求模型 、說明接口，并進行中間設計和實現(xiàn)； ? B語言就是 AMN（抽象機器符號）， AMN支持規(guī)格說明的類型檢測、動態(tài)驗證、數(shù)學證明等來確保設計過程的正確。 6. 形式化程序規(guī)范描述語言簡介－ B語言簡介 2 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 20 程序規(guī)范與程序 (續(xù) ) ? B方法的特點 –簡單熟悉的符號表示法 ：這種符號表示法用來表達狀態(tài)轉(zhuǎn)換，從規(guī)格說明到編碼，這種統(tǒng)一的形式減少了學習的難度和轉(zhuǎn)換中的語法錯誤。 –模塊化構(gòu)造 ：從規(guī)格說明到實現(xiàn)的模塊化構(gòu)造允許將規(guī)格說明和驗證過程分解為多個子任務來進行。 –大量實用的工具支持 ：現(xiàn)有大量的實用工具支持了 B方法軟件開發(fā)周期的所有階段，包括動畫和文檔生成。 –成功的工業(yè)應用 ： B語言和方法已在很多的工業(yè)領域得到成功應用，包括實時、仿真、信息處理和工程等。 6. 形式化程序規(guī)范描述語言簡介－ B語言簡介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 21 程序規(guī)范與程序 (續(xù) ) 6. Z語言、 VDM、 B形式化方法的比較 屬性 Z VDM B 基礎 謂詞演算 , 集合論 , 模式 偏函數(shù) , 集合論 最弱前置條件 , 集合論 開發(fā)階段 規(guī)范說明 規(guī)范說明 , 設計 規(guī)范說明 , 設計 , 實現(xiàn) 形式 模式的符號表示 , 關系 前 /后置條件 , 函數(shù) 嚴格的編程語言 工具支持 在規(guī)格說明級 在規(guī)格說明級 BToolkit,AtchierB,所有開發(fā)階段 培訓支持 圖書、課程 圖書 , 課程 實例研究、課程 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 22 內(nèi)容－ Where we are？ ? 程序規(guī)范、規(guī)范的描述 ? 斷言與規(guī)范及 {P} S {Q} ? 程序正確性的概念 ? 程序正確性證明的過程 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 23 斷言與規(guī)范 1. 斷言 – 斷言就是關于事物性質(zhì)的陳述 。這個陳述可真可假。如“ 三是個質(zhì)數(shù) ” – 用斷言作為程序的注解或作為正確性命題的一部分時，常用大括號括起來。 – 例 1：寫一個計算商和余數(shù)的程序 ?程序規(guī)范： “ 設被除數(shù) x1是個非負整數(shù)，除數(shù) x2是個正整數(shù)，計算 x1除以 x2的商 y1和余數(shù) y2” ?又描述為： “ 初始條件： {x1=0 AND x20}, 計算滿足 {x1=x2*y1+y2 and 0=y2x2}的整數(shù) y1和 y2” 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 24 斷言與規(guī)范 (續(xù) ) 一般地，一個程序規(guī)范可表示為由兩個謂詞構(gòu)成的二元組（ P， Q）。其中， ? P描述了所欲求解的問題必須滿足的 初始條件 ，它限定了輸入?yún)?shù)的性質(zhì)，稱為初始斷言或前置斷言； ? Q描述了問題的 最終解必須滿足的性質(zhì) ，稱為結(jié)果斷言或后置斷言。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserved 25 斷言與規(guī)范 (續(xù) ) ? 程序斷言是對程序的性質(zhì)的陳述。 ? 最重要的一個程序斷言為： {P} S {Q}。 其中，（ P， Q）是程序 S的程序規(guī)范， S是一個程序（或語句） ? 斷言 {P} S {Q}稱為 S關于（ P， Q）的正確性斷言。 ? 它的意義： “ 若 S開始執(zhí)行時 P為真，則 S的執(zhí)行必終止且終止時 Q為真 ” 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學院計算機軟件所 程序設計方法學 All Rights Reserve
環(huán)評公示相關推薦
鄂ICP備17016276號-1