pm-06-chap03-程序規(guī)范及其正確性證明概述-文庫吧
2025-07-20 10:35 本頁面
【正文】 構(gòu)給出。 ? Ｚ規(guī)格說明由一系列模式組成，每個模式定義一個抽象對象或操作，并用謂詞判定描述給出新的對象或操作的語義約束。 ? 模式例 : 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 3 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 11 程序規(guī)范與程序 (續(xù) ) ? 模式例 1: [Student] // 引入基本類型 student StudentSys //模式名 Enrolled,tested: P Student // 聲明部分 , 學(xué)生的密集類型 enrolled ≤size // 斷言部分，合取關(guān)系 tested ? enrolled 等價于： //水平方式 StudentSys=[enrolled,tested: P Student | enrolled ≤size ? tested ? enrolled ] 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 4 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 12 程序規(guī)范與程序 (續(xù) ) ? 模式例 2: EnrollStudent ?StudentSys // = Studentsys ? StudentSys’的簡寫 name?: Student // 在輸入變量后加？ name? ? enrolled // 在輸出變量后加！ enrolled size // 帶有后綴‘的變量表示操作后的變量 enrolled’ = enrolled ∪ {name?} tested’= tested 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 5 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 13 程序規(guī)范與程序 (續(xù) ) ? 缺點 : ⑴ Ｚ語言對大型系統(tǒng)的模塊化能力不足。 ⑵ 難以識別影響某一狀態(tài)模式的所有操作模式。 ⑶ 不能支持規(guī)格說明的重用。 ⑷ Ｚ語言難以由計算機(jī)直接處理。 – 缺少商品化的工具支持等到諸多原因 6. 形式化程序規(guī)范描述語言簡介－ Z語言簡介 6 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 14 程序規(guī)范與程序 (續(xù) ) ? VDM（ Vienna Development Method）是在 1969年為開發(fā) PL/1語言時，由 IBM公司維也納實驗室 的研究小組提出的。初衷是為了描述 PL/1語言的語義。 ? VDM是一種 功能構(gòu)造性規(guī)格說明技術(shù) ，它通過 一階謂詞邏輯和已建立的抽象數(shù)據(jù)類型 來描述每個運算或函數(shù)的功能。 ? 這種方法在 90年代初在歐美許多研究機(jī)構(gòu)或大學(xué)得到了廣泛的應(yīng)用。如曼徹斯特大學(xué)將其作為 CS的必修課。 ? 1996年 ISO制訂了 VDM的國際標(biāo)準(zhǔn)化版本 VDMSL 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 1 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 15 程序規(guī)范與程序 (續(xù) ) ? VDM技術(shù)的基本思想： – 運用 抽象數(shù)據(jù)類型、數(shù)學(xué)概念和符號 來規(guī)定運算或函數(shù)的功能； ? 可使軟件系統(tǒng)的功能描述在 抽象級 上進(jìn)行，完全擺脫了實現(xiàn)細(xì)節(jié)，這樣為軟件實現(xiàn)者提供了很大的靈活性； ? 這種形式化規(guī)格說明還為 程序正確性證明 提供了依據(jù)。 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 2 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌 東大信息學(xué)院計算機(jī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 16 程序規(guī)范與程序 (續(xù) ) ? VDM支持兩種抽象： 數(shù)據(jù)抽象和操作抽象 。 ? 一個 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ī)軟件所 程序設(shè)計方法學(xué) All Rights Reserved 17 程序規(guī)范與程序 (續(xù) ) ? 缺點： ⑴ 由于 VDM對抽象數(shù)據(jù)類型預(yù)先定義了運算，而某些用戶定義的類型在規(guī)格說明描述中無需這么多運算，因而產(chǎn)生了 運算冗余 。 ⑵ VDM目前還 未能建立一整套描述機(jī)制 ，將一個大型系統(tǒng)分解為許多運算而描述出這些運算之間的關(guān)系 ⑶ VDM形式規(guī)格說明 過于形式化 不容易理解 6. 形式化程序規(guī)范描述語言簡介－ VDM簡介 4 第 3章 程序規(guī)范及其正確性證明概述 2022年 3月 3日星期四 鮑玉斌
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1