pm-06-chap03-程序規(guī)范及其正確性證明概述(已修改)
2025-08-16 10:35 本頁面
【正文】 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ì)之前，第一步必須明確 “ 做什么 ” 。 – 所謂 “ 做什么 ” 是指對欲求解的問題的描述。 – 程序規(guī)范（ PSProgram Specification） :關(guān)于 “ 做什么 ”的描述。 ? 這里的 PS僅指功能的描述，不包括諸如處理速度、執(zhí)行時(shí)間、響應(yīng)周期等與時(shí)間有關(guān)性能指標(biāo)。 – PS是軟件工程的需求分析的結(jié)果。 – PS的含義是映射，是輸入到輸出的映射，它反映了程序?qū)?shù)據(jù)的作用。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 4 程序規(guī)范與程序 (續(xù) ) 2. 程序 – 程序也是映射，是 輸入到計(jì)算的映射 ，即每一輸入都對應(yīng)一串計(jì)算步。 3. 程序規(guī)范與程序的關(guān)系 – 給出規(guī)范后，程序開發(fā)就是建立一個(gè)程序，使得計(jì)算剛好能實(shí)現(xiàn)規(guī)范的映射； – 程序驗(yàn)證是 證明程序正確地實(shí)現(xiàn)了規(guī)范 ，即證明規(guī)范和已有程序之間的一致性 規(guī)范 程序 輸入 輸出 映射 輸入 計(jì)算 映射 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 5 程序規(guī)范與程序 (續(xù) ) 4. 程序規(guī)范的描述 規(guī)范語言 – 規(guī)范必須用語言描述，該語言稱為規(guī)范語言。 – 描述一個(gè)復(fù)雜問題的輸入和輸出之間的關(guān)系是困難的，目前對規(guī)范語言的模式尚無定論。有三種模式： – 自然語言： 不夠準(zhǔn)確，存在二義性，必須輔以數(shù)學(xué)語言。 – 一階謂詞 ：可以精確地描述問題的輸入和輸出的關(guān)系，但是規(guī)范文本比較長。如 Hoare系統(tǒng)。 – 數(shù)學(xué)語言： 用數(shù)學(xué)語言可以把輸入和輸出的映射描述為函數(shù)。這些函數(shù)的精確的泛函定義就構(gòu)成了問題的規(guī)范。但存在 過于規(guī)范 的問題。 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 6 程序規(guī)范與程序 (續(xù) ) 5. 一個(gè)合適的程序規(guī)范語言應(yīng)滿足的基本條件 : – 應(yīng)當(dāng)為描述者和使用者所直接理解； – 應(yīng)當(dāng)有嚴(yán)格的數(shù)學(xué)語義 – 應(yīng)當(dāng)與形式方法的構(gòu)造理論和程序設(shè)計(jì)語言協(xié)調(diào) – 應(yīng)當(dāng)有較強(qiáng)的表達(dá)能力和通用性 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 7 程序規(guī)范與程序 (續(xù) ) ? Z語言 ? VDM ? B方法 ? 三者的比較 6. 形式化程序規(guī)范描述語言簡介 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 8 程序規(guī)范與程序 (續(xù) ) ? Z語言是一種基于 集合論和一階謂詞邏輯 的形式化語言； ? Z語言支持軟件的 形式化規(guī)范描述，規(guī)范的推理和求精 ； ? 是迄今為止應(yīng)用最廣泛的形式語言之一； ? Z是在 Jean Raymond Abrial等的開創(chuàng)性工作下，由英國牛津大學(xué)的程序設(shè)計(jì)研究小組（ PRG， Programming Research Group），于 20世紀(jì) 80年代初開發(fā)； ? PRG與 IBM的 Hursley實(shí)驗(yàn)室合作， 將 Z語言用于 IBM的客戶信息控制系統(tǒng)的開發(fā) ，使得最終的 產(chǎn)品質(zhì)量 得到了全面的的提高，所測出的錯(cuò)誤數(shù)量大大減少，并且整體開發(fā)費(fèi)用 降低了 9％ ； ? 在 ISO指導(dǎo)下的國際標(biāo)準(zhǔn)化 Z工作于 2022年完成 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計(jì)算機(jī)軟件所 程序設(shè)計(jì)方法學(xué) All Rights Reserved 9 程序規(guī)范與程序 (續(xù) ) ? 提供了一種稱為 模式（ Schema）的結(jié)構(gòu) ，它是Z的基本描述單位，以此來描述一個(gè)規(guī)范說明的狀態(tài)空間（靜態(tài)性質(zhì)）和操作（動態(tài)行為） 。 ? Ｚ語言的模式和模式演算： – 狀態(tài)模式 對目標(biāo)軟件系統(tǒng)的 結(jié)構(gòu)特征 進(jìn)行抽象描述； – 操作模式 對目標(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ù) ) ? Ｚ模式說明可以 組合成新的Ｚ模式 ，新的Ｚ模式繼承其成分模式的一切屬性和約束。軟件系統(tǒng)的Ｚ模式規(guī)格說明可以按一定的層次結(jié)
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1