程序設(shè)計(jì)方法學(xué) 課件

第六章

程序設(shè)計(jì)的形式化方法

軟件新技術(shù)智能化技術(shù)擴(kuò)大軟件功能的關(guān)鍵途徑自動(dòng)化技術(shù)提高軟件生產(chǎn)率的根本途徑集成化技術(shù)助于提高生產(chǎn)率、提高質(zhì)量并行化技術(shù)提高系統(tǒng)實(shí)效的關(guān)鍵技術(shù)自然化技術(shù)實(shí)現(xiàn)社會(huì)信息化2/9/20231華東師大計(jì)算機(jī)科學(xué)技術(shù)系重要方向 攻克的關(guān)鍵教技術(shù)網(wǎng)絡(luò)體系傳感器網(wǎng)與因特網(wǎng)的高效融合集成芯片從Systemonchip到Chipondemount虛擬計(jì)算資源聚合的有效性和可靠性驗(yàn)證軟件工程基于網(wǎng)絡(luò)環(huán)境的需求工程知識(shí)處理挖掘從消息到知識(shí)到?jīng)Q策的元知識(shí)高效系統(tǒng)在高性（效）能計(jì)算系統(tǒng)中系列關(guān)注 信息安全 信息教育2/9/20232華東師大計(jì)算機(jī)科學(xué)技術(shù)系跨越源之識(shí)規(guī)律創(chuàng)新根植辨短長(zhǎng)汪成為院士2/9/20233華東師大計(jì)算機(jī)科學(xué)技術(shù)系§1概述一、重要意義

軟件發(fā)展中的問題：整體功能不強(qiáng)、缺乏智能、質(zhì)量欠佳、生產(chǎn)效率低軟件自動(dòng)化是提高軟件生產(chǎn)率的根本途徑軟件自動(dòng)化的前提是形式化因此將形式化的理論和方法用于需求分析與規(guī)格說明是實(shí)現(xiàn)軟件自動(dòng)化的前提2/9/20235華東師大計(jì)算機(jī)科學(xué)技術(shù)系二、發(fā)展?fàn)顩r有30多年歷史 Dijkstra、Hoare ――――程序驗(yàn)證Scott、Stratchey ――――程序語義

形式化方法(FormalMethod)： 通過嚴(yán)格的規(guī)范化的數(shù)學(xué)理論來描述軟件系統(tǒng)“做什么”的方法。需要形式規(guī)范語言的支持。形式規(guī)范語言： 提供了一個(gè)稱為語法域的記號(hào)系統(tǒng)。一個(gè)稱為語義域的目標(biāo)集合，以及一組精確定義的哪些目標(biāo)系統(tǒng)滿足那個(gè)規(guī)范的規(guī)則。

2/9/20236華東師大計(jì)算機(jī)科學(xué)技術(shù)系因此，形式化方法是在軟件系統(tǒng)的開發(fā)過程中使用一種形式系統(tǒng)來表示模型的方法。形式系統(tǒng)是二元組（L，Cn）L：語言（形式規(guī)范語言）Cn：對(duì)應(yīng)關(guān)系，由推理規(guī)則構(gòu)成在軟件規(guī)范方法方面的代表性成果有：⑴基于異調(diào)代數(shù)的代數(shù)方法 特點(diǎn)：用抽象代數(shù)中的公理化方法來刻畫抽象數(shù) 據(jù)類型中運(yùn)算的性質(zhì)，而不涉及數(shù)據(jù)的具 體表示。 基本理論：代數(shù)語義2/9/20237華東師大計(jì)算機(jī)科學(xué)技術(shù)系在軟件規(guī)范語言方面的代表性成果有： 一階謂詞演算組成語言 80年代：Z語言、Larch語言、VDM語言90年代：面向?qū)崟r(shí)及分布式的LOTOS語言、 面向?qū)ο蟮腪++、Object-Z、VDM++等三、分類⑴ 基于模型的方法 給出系統(tǒng)（程序）狀態(tài)和狀態(tài)變換與操作的顯式的表示但亦是抽象的定義，不涉及并發(fā)的行為。如：Z、VDM2/9/20239華東師大計(jì)算機(jī)科學(xué)技術(shù)系⑵ 代數(shù)方法 通過聯(lián)系不同的操作間的行為關(guān)系給出操作的隱式定義，未給出并發(fā)的顯式表示。

如：OBJ、Larch⑶ 過程代數(shù)方法 給出并發(fā)過程的一個(gè)顯式模型，并通過過程間允許的可觀察的通信上的限制來約束表示行為。 如：CSP（通信順序進(jìn)程）和CCS（通信系統(tǒng)計(jì)算）⑷ 基于邏輯的方法 采用邏輯來描述系統(tǒng)的特性，包括程序行為的低級(jí)規(guī)范和系統(tǒng)時(shí)間的行為規(guī)范。 如：時(shí)態(tài)邏輯、模態(tài)邏輯2/9/202310華東師大計(jì)算機(jī)科學(xué)技術(shù)系⑸ 基于網(wǎng)絡(luò)的方法 根據(jù)網(wǎng)絡(luò)中的數(shù)據(jù)流顯式地給出系統(tǒng)的并發(fā)模型，包括數(shù)據(jù)從一個(gè)結(jié)點(diǎn)流向另一個(gè)結(jié)點(diǎn)的條件。

如：Petri網(wǎng)、謂詞變換網(wǎng)

2/9/202311華東師大計(jì)算機(jī)科學(xué)技術(shù)系三項(xiàng)任務(wù)分別對(duì)應(yīng)三方面的活動(dòng)：1. 形式化規(guī)范（規(guī)格）：軟件規(guī)范是指對(duì)軟件系統(tǒng)對(duì)象及用來對(duì)系統(tǒng)對(duì)象進(jìn)行操作的方法的集合。以及對(duì)所開發(fā)系統(tǒng)中的各對(duì)象在生命周期間的集體行為的描述。對(duì)應(yīng)與軟件生命周期的各個(gè)階段，規(guī)范應(yīng)該理解為是一個(gè)多階段的行為。見例圖規(guī)范可以采用非、半形式化的方法來描述，形式化規(guī)范精確地描述了用戶的需求、軟件系統(tǒng)的功能及各種性質(zhì)，其描述的是“做什么”，而不考慮“如何做”。因此，在理解、掌握形式規(guī)范語言和方法的基礎(chǔ)上對(duì)所描述的系統(tǒng)的全面、深入的了解，給出恰如其分的描述上至關(guān)重要的。2/9/202313華東師大計(jì)算機(jī)科學(xué)技術(shù)系包含各規(guī)格階段的生命周期模型例需求分析BSSRD系統(tǒng)設(shè)計(jì)1DS系統(tǒng)設(shè)計(jì)2PS軟件開發(fā)代碼實(shí)現(xiàn)軟件測(cè)試運(yùn)行SRD：軟件需求文檔 BS：行為規(guī)范DS：設(shè)計(jì)規(guī)范 PS：程序規(guī)范2/9/202314華東師大計(jì)算機(jī)科學(xué)技術(shù)系軟件系統(tǒng)規(guī)范的形式化方法從形式化規(guī)范到目標(biāo)軟件系統(tǒng)的可實(shí)現(xiàn)和可執(zhí)行角度，可分為三類：操作類：此類方法基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜態(tài)分析和模型執(zhí)行而得到驗(yàn)證。如：有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)等。描述類：此類方法基于數(shù)學(xué)公理和概念，通過邏輯或代數(shù)給出系統(tǒng)狀態(tài)空間，具有高度抽象的特點(diǎn)，便于通過自動(dòng)工具進(jìn)行驗(yàn)證。如：基于代數(shù)的Z、VDM、Larch等，基于邏輯的命題線性時(shí)態(tài)邏輯、一階線性時(shí)態(tài)邏輯、計(jì)算樹邏輯等。雙重類：此類方法兼具二者的特點(diǎn)，如：擴(kuò)展?fàn)顟B(tài)機(jī)/實(shí)時(shí)時(shí)態(tài)邏輯等。2/9/202315華東師大計(jì)算機(jī)科學(xué)技術(shù)系形式化驗(yàn)證軟件開發(fā)中錯(cuò)誤發(fā)現(xiàn)的越晚修改的代價(jià)越大，與傳統(tǒng)方法不同的是形式化方法要求在完成形式規(guī)范后就進(jìn)行形式驗(yàn)證。形式驗(yàn)證主要技術(shù)包括模型檢驗(yàn)和定理證明。模型驗(yàn)證是一種基于有限狀態(tài)機(jī)模型并檢驗(yàn)該模型的期望特性的技術(shù)。即對(duì)模型的狀態(tài)空間進(jìn)行搜索，以確認(rèn)該系統(tǒng)具有某些性質(zhì)。終止性依賴于模型的有限性。優(yōu)點(diǎn)是：完全自動(dòng)化、速度快，可用于系統(tǒng)的部分規(guī)范。缺點(diǎn)是：“狀態(tài)爆炸問題”因而極大地限制其實(shí)際使用范圍。有序二叉決策圖（OrderedBinaryDecisionDiagrams)是一種表述狀態(tài)轉(zhuǎn)移系統(tǒng)的高效率的方法。目前可以處理100～200個(gè)狀態(tài)變量、狀態(tài)數(shù)達(dá)10120的系統(tǒng)。2/9/202317華東師大計(jì)算機(jī)科學(xué)技術(shù)系模型檢驗(yàn)需要工具的支持，已有的工具有： 時(shí)態(tài)邏輯模型檢驗(yàn)工具，如：EMC、CESAR、 SMV、Nurphi、SPIN、UV等。 行為一致檢驗(yàn)工具，如：FRD、Cospan/Formal Check等復(fù)合檢驗(yàn)工具，如：HSIS、VIS、STcP等貝爾實(shí)驗(yàn)室用FormalCheck對(duì)其高級(jí)數(shù)據(jù)鏈路控制器進(jìn)行驗(yàn)證，從6個(gè)性能的規(guī)范中發(fā)現(xiàn)一個(gè)失敗，進(jìn)而發(fā)現(xiàn)一個(gè)影響信道流量的Bug。基于SMV輸入語言建立了IEEEFuturebus＋896.1－1991標(biāo)準(zhǔn)下cache一致協(xié)議精確模型，通過SMV的驗(yàn)證，發(fā)現(xiàn)了原先未找到和潛在的錯(cuò)誤。此工作是第一次從IEEE標(biāo)準(zhǔn)中發(fā)現(xiàn)錯(cuò)誤。2/9/202318華東師大計(jì)算機(jī)科學(xué)技術(shù)系定理證明采用邏輯公式來規(guī)范系統(tǒng)及其性質(zhì)，這兒的邏輯由一個(gè)具有公理或推理規(guī)則的形式系統(tǒng)給出，進(jìn)行定理證明的過程就是應(yīng)用這些公理或推理規(guī)則來證明系統(tǒng)具有某些性質(zhì)。定理證明可以處理無限狀態(tài)空間問題，粗略地分為自動(dòng)和交互兩種類型，自動(dòng)定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功。交互式定理證明系統(tǒng)需要與用戶進(jìn)行交互，要求用戶能提供驗(yàn)證中創(chuàng)造性最強(qiáng)的部分（如斷言等），因此效率較低，較難用于大系統(tǒng)的驗(yàn)證。2/9/202319華東師大計(jì)算機(jī)科學(xué)技術(shù)系程序求精（又稱程序變換） 是將自動(dòng)推理和形式化方法相結(jié)合而形成的一門新技術(shù)，研究從抽象的形式規(guī)范推演出具體的面向計(jì)算機(jī)的程序代碼的全過程?；舅枷胧牵河靡粋€(gè)抽象程度低、過程性強(qiáng)的程序去替代一個(gè)抽象程度高、過程性弱的程序，并保持二者功能的一致性。這兒的“程序”是廣義的“程序”，是對(duì)規(guī)范、設(shè)計(jì)文檔、程序代碼的統(tǒng)稱。按這種觀點(diǎn)，程序開發(fā)的過程就是從最高層的程序開始，通過一系列的求精變換，每一次都降低一些抽象程度或增加一些可執(zhí)行性，最終得到能指導(dǎo)計(jì)算機(jī)明確執(zhí)行的程序代碼。2/9/202321華東師大計(jì)算機(jī)科學(xué)技術(shù)系在進(jìn)行求精的過程中必須要保證程序的正確性，即保證程序是滿足最初的形式規(guī)范的。程序的這種正確性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可以采用驗(yàn)證工具來證明。程序求精技術(shù)是形式化方法研究的一個(gè)熱點(diǎn)，盡管目前真正用于實(shí)際軟件開發(fā)過程中并不多，但是這是一個(gè)很重要的方向。典型的方法有：IBMHursley公司和牛津大學(xué)PRG程序設(shè)計(jì)研究組提出的針對(duì)Z規(guī)范的求精方法，CarrollMorgan的規(guī)則求精方案（見ProgrammingfromSpecifications一書）。2/9/202322華東師大計(jì)算機(jī)科學(xué)技術(shù)系五、認(rèn)識(shí)形式化方法成長(zhǎng)至今爭(zhēng)議聲不斷，應(yīng)正確地認(rèn)識(shí)形式化方法，在結(jié)合到具體的軟件開發(fā)過程時(shí)應(yīng)考慮：應(yīng)用的類型，考慮問題領(lǐng)域的特點(diǎn)和模型的復(fù)雜性規(guī)模和結(jié)構(gòu)，較適應(yīng)中等規(guī)模的系統(tǒng)，大型系統(tǒng)應(yīng)考慮具有良好的結(jié)構(gòu)類型的選擇，應(yīng)從所確定的目標(biāo)出發(fā)考慮采用的形式化方法的類型形式化的級(jí)別，應(yīng)先確定應(yīng)用的關(guān)鍵程度、項(xiàng)目規(guī)模、可用資源等確定采用非、半或高度形式化的描述2/9/202323華東師大計(jì)算機(jī)科學(xué)技術(shù)系2/9/202325華東師大計(jì)算機(jī)科學(xué)技術(shù)系結(jié)論：

形式化的方法不是靈丹妙藥，

而是一種改進(jìn)系統(tǒng)可靠性的方法。

2/9/202326華東師大計(jì)算機(jī)科學(xué)技術(shù)系一．OBJ簡(jiǎn)介一種代數(shù)形式規(guī)范語言，最基本的概念是ADT（抽象數(shù)據(jù)類型），每個(gè)ADT描述一個(gè)客體。具有很強(qiáng)的獨(dú)立定義和數(shù)據(jù)抽象的機(jī)制。支持層次化設(shè)計(jì)，即在定義高層ADT時(shí)可以使用下層已定義的ADT。用OBJ書寫形式規(guī)范的過程就是用代數(shù)等式（方程）定義ADT的過程。是一種基于代數(shù)方程邏輯的代數(shù)形式語義，又具有一種基于把代數(shù)方程解釋為重寫規(guī)則的操作語義。（可利用這種語義證明程序的正確性）。

2/9/202329華東師大計(jì)算機(jī)科學(xué)技術(shù)系二、基本形式一個(gè)OBJ的形式規(guī)范說明是諸多ADT定義的集合，每個(gè)ADT具有如下形式：其中obj與jbo是必須的，其余部分任選。2/9/202330華東師大計(jì)算機(jī)科學(xué)技術(shù)系例1．定義ADTNATURALobjNATURALsortsnatops0:

nat/*0無定義域，常量*/succ(-):natnat/*nat上的一目運(yùn)算，‘-’表示運(yùn) 算對(duì)象*/jbo在定義ADT時(shí)若需要用到低層已定義ADTL中的運(yùn)算，可在obj處用/L指出，多個(gè)時(shí)用空格分隔。例子2/9/202331華東師大計(jì)算機(jī)科學(xué)技術(shù)系例2.在NATURAL的基礎(chǔ)上定義ADDobjADD/NATURALops-+-:natnatnatvarsx,y:nateqns(0+x=x)(succ(x)+y=succ(x+y))jbo下面將給出一個(gè)較大的形式規(guī)范定義——對(duì)整數(shù)序列進(jìn)行分類。在規(guī)范中自底向上的順序分別定義了多個(gè)ADT。如：Boolean、Integer、seq_INT、sort_seq_INT等。2/9/202332華東師大計(jì)算機(jī)科學(xué)技術(shù)系例3．對(duì)一個(gè)整型數(shù)列分類的形式規(guī)范1. obj Boolean/TRUTH//TRUTH是OBJ內(nèi)部已 vars a:Boolean //定義的ADT，它具有eqns (not(T)=F) //T和F兩個(gè)常量 (not(F)=T) (not(not(a))=a) (Tanda=a) (aandF=F) (Tora=T) (Fora=a)jbo2/9/202333華東師大計(jì)算機(jī)科學(xué)技術(shù)系2.整型ADT //對(duì)下述十個(gè)運(yùn)算的規(guī)則容易給出，故省略了obj Integer/Booleansorts INTops --: INTINT -+-: INTINTINT ---: INTINTINT -*-: INTINTINT -div-: INTINTINT -mod-: INTINTINT -<-: INTINTBoolean ->-: INTINTBoolean -<=-: INTINTBoolean ->=-: INTINTBooleanjbo2/9/202334華東師大計(jì)算機(jī)科學(xué)技術(shù)系3.定義整型字符串ADTobj seq_INT/Integersorts seq_INTops []:seq_INT //空 [-]:seq_INT //常量--:seq_INTseq_INTseq_INT //鏈接hd-:seq_INTINT //頭元素tl-:seq_INTseq_INT //尾串len-:seq_INTINT //長(zhǎng)度vars i:INT s:seq_INT2/9/202335華東師大計(jì)算機(jī)科學(xué)技術(shù)系eqns ([]s=s) (s[]=s) (hd[]=0) (hd[i]=i) (hd([i]s)=i) (tl[]=[]) (tl[i]=[]) (tl([i]s)=s) (len[]=0) (lens=succ(len(tls)ifs≠[]))jbo2/9/202336華東師大計(jì)算機(jī)科學(xué)技術(shù)系4．定義比較ADTobj sort_seq_split/seq_INTIntegerops-<-: seq_INT,INTseq_INT ->=-:seq_INT,INTseq_INTvars s:seq_INT i,x:INTeqns ([]<x=[]) ([i]<x=[]ifi>=x) ([i]<x=[i]ifi<x) (([i]s)<x=s<xifi>=x)(([i]s)<x=[i]s<xifi<x) ([]>=x=[]) ([i]>=x=[]ifi<x) (([i]s)>=x=[i](s>=x)ifi>=x)jbo2/9/202337華東師大計(jì)算機(jī)科學(xué)技術(shù)系5．定義分類ADT的規(guī)范objsort_seq_INT/sort_seg_splitseq_INTIntegerBooleanops sort-: seq_INTseq_INT is_sorted-:seq_INTBooleanvars s,s1,s2:seq_INTi,j,x:INTeqns (is_sorted[]=T) (is_sorted[i]=T) (is_sorted[i][j]=i<=j) (is_sorted[i][j]s=i<=jandis_sorted([j]s)) (sorts=sifis_sorteds)2/9/202338華東師大計(jì)算機(jī)科學(xué)技術(shù)系(sort([i][j])=sort([j][i])ifi>j)(sort([i][j])s=sort([j][i]s)ifi>j)(sort(s[i][j])=sort(s[j][i])ifi>j)(sort(s1[i][j]s2)=sort(s1[j][i]s2ifi>j)((sort(tls<hds))[hds](sort(tls>=hds)) =sortsifs≠[])(s>=x=(tls>=x)ifs≠[]andhds<x)(s>=x=[hds](tls>=x)ifs≠[]andhds>=x)(s<x=(tls<x)ifs≠[]andhds>=x)(s<x=[hds](tls<x)ifs≠[]andhds<x)jbo2/9/202339華東師大計(jì)算機(jī)科學(xué)技術(shù)系三、運(yùn)算的性質(zhì)從功能上可以將運(yùn)算分為四類：初始化運(yùn)算 不以任何別的類型客體作為它的輸入，其結(jié)果是具有自身類型的值。 如：seq_INT[-]2.構(gòu)造運(yùn)算 以自身類型客體和別的類型客體為輸入，產(chǎn)生具有自身類型的結(jié)果。 如：--3.修改運(yùn)算 修改自身類型客體的變量 如：tl–4.觀察運(yùn)算以自身類型客體為輸入，得出具有別的類型客體的結(jié)果。

如：len–2/9/202340華東師大計(jì)算機(jī)科學(xué)技術(shù)系四、抽象的計(jì)算程序

例4．定義自然數(shù)類型的棧運(yùn)算的ADT obj Stack/IntegerBooleansorts stackops create: stack /*空棧*/ push--:stackINTstack pop-:stackstack top-:stackINT∪{ERR} empty-:stackBoolean2/9/202341華東師大計(jì)算機(jī)科學(xué)技術(shù)系vars s:stack n:INTeqns (empty(create)=T) (empty(pushs,n)=F) (pop(create)=create) (pop(push(s,n)=s) (top(create)=ERR) (top(push(s,n)=n)jbo2/9/202342華東師大計(jì)算機(jī)科學(xué)技術(shù)系抽象計(jì)算程序的計(jì)算可以歸結(jié)為代數(shù)系統(tǒng)中的重寫規(guī)則的應(yīng)用，而得到計(jì)算的結(jié)果。例5：設(shè)抽象計(jì)算程序?yàn)椋?create() push(s,5) push(s,3) pop(s) top(s)則top(s)=top(pop(s))=top(pop(push(s,3))) =top(pop(push(push(s,5),3))=top(push(s,5))=5由此可知，這種方法可以機(jī)械執(zhí)行。2/9/202343華東師大計(jì)算機(jī)科學(xué)技術(shù)系正確性證明依賴相應(yīng)的ADT中定義的運(yùn)算規(guī)范，可以證明程序的正確性。方法為：將代數(shù)等式視為重寫規(guī)則，即將等式L=R視為L(zhǎng)R（L被定義為R）。就可以用于程序的正確性證明。2/9/202344華東師大計(jì)算機(jī)科學(xué)技術(shù)系§3.基于模型方法的規(guī)范語言VDM

TheViennaDevelopmentMethod

一、概況VDM由IBM的Vienna實(shí)驗(yàn)室20世紀(jì)70年代提出的的一種形式化方法。最初是為了解決用形式化方法來開發(fā)編譯系統(tǒng)，使語言的語法、語義的定義更為嚴(yán)格、更加系統(tǒng)化（如實(shí)現(xiàn)PL/1語言的語義規(guī)范）。當(dāng)時(shí)用VDL用于語言的注釋。得到廣泛的應(yīng)用VDM在歐洲得到發(fā)展，從70年代末到90年代在歐美許多研究機(jī)構(gòu)和大學(xué)得到廣泛的應(yīng)用（如曼徹斯特大學(xué)講其作為必修課），以后逐漸稱為一般的軟件開發(fā)方法。2/9/202345華東師大計(jì)算機(jī)科學(xué)技術(shù)系1996年國(guó)際標(biāo)準(zhǔn)化組織（ISO）制定了VDM的國(guó)際化版本VDM－SL（VDMSpecificationLanguage)。目前VDM已稱為應(yīng)用最為廣泛的形式化規(guī)范語言。VDM是一種功能構(gòu)造性規(guī)范技術(shù)。由一階謂詞邏輯和已經(jīng)建立的ADT來描述每個(gè)運(yùn)算或函數(shù)的功能?；舅枷胧茿DT、數(shù)學(xué)概念和符號(hào)來規(guī)定運(yùn)算或函數(shù)的功能，而且這種規(guī)定的過程是結(jié)構(gòu)化的，其目的是要在系統(tǒng)實(shí)現(xiàn)之前簡(jiǎn)單而又明確地指出軟件系統(tǒng)要完成的功能。支持程序正確性的證明。用Hoare的前/后斷言描述運(yùn)算的規(guī)范。2/9/202346華東師大計(jì)算機(jī)科學(xué)技術(shù)系二、VDM的形式規(guī)范的基本組成形式VDM形式規(guī)范由三部分組成： 狀態(tài)、類型不變式、運(yùn)算功能是一種基于抽象模型的方法， 由： 表示（數(shù)據(jù)）抽象——系統(tǒng)的狀態(tài)描述 和 運(yùn)算（操作）抽象——用前/后斷言 所組成。模型規(guī)范的形式定義： M=(，0,，Ω) 是M的狀態(tài)集（含有不變式） 0是初始狀態(tài) Ω是運(yùn)算集合 其實(shí)質(zhì)是將軟件系統(tǒng)視為基本狀態(tài)的運(yùn)算類型。2/9/202347華東師大計(jì)算機(jī)科學(xué)技術(shù)系1、系統(tǒng)狀態(tài)規(guī)則基本形式：類型ID=類型定義實(shí)體 其中：ID是新定義的一個(gè)類型名 實(shí)體是基本類型定義的一個(gè)新類型?；绢愋停?①基本型：N,R,B(自然數(shù)，實(shí)數(shù)，Boolean) 運(yùn)算是常見的算術(shù)和邏輯運(yùn)算 ②集合型：形式為：X=setofQ Q是已定義類型或基本類型，X是集合型ID 運(yùn)算有：并（）、交（）、差（/）、元素個(gè)數(shù)（card）、屬于（）、子集（）、真子集（）等

2/9/202348華東師大計(jì)算機(jī)科學(xué)技術(shù)系③表型：有序集合，每個(gè)元素有確定位置，可重復(fù)出現(xiàn)，定義形式為：S=seqofQS為新類型的ID，Q為S的元素類型運(yùn)算有：求頭（hd）、求尾（tl)、長(zhǎng)度（len)、連接（conj）、元素集（elem)、索引集（inds)等④映射：有限、可列集的一個(gè)函數(shù)，通常以對(duì)偶集合形式表示，定義形式為：M=MapofQM為新類型的ID，Q為M的元素類型 運(yùn)算有：求定義域（dom），求值域（rng） 限定定義域（△），定義域元素刪除（）等2/9/202349華東師大計(jì)算機(jī)科學(xué)技術(shù)系⑤復(fù)合型：P=ComposePof e1:Q1

…… e2:Q2 end P為新類型的ID，ei、Qi（i=1……）分別為P的分量名和分量類型 運(yùn)算：求復(fù)合類型值（mk_P）、改變分量值、求分量的值。2/9/202350華東師大計(jì)算機(jī)科學(xué)技術(shù)系例１一個(gè)教師職稱提升系統(tǒng)的ADT定義Studentdata=ComposeStudentdataof Name:String T_score_list:SeqofChoice endResearchdata=ComposeResearchdataof Name1:String R_Score_List:SeqofN endTeacher=ComposeTeacherof T_name:String T_score:R R_score:R end2/9/202351華東師大計(jì)算機(jī)科學(xué)技術(shù)系2、類型不變式規(guī)則類型不變式是指對(duì)狀態(tài)規(guī)則中規(guī)定的類型給出其應(yīng)滿足的性質(zhì)。表示形式： 設(shè)ST是在類型規(guī)范中所定義的一個(gè)類型ID。 Inv_ST(S)=P(S)其中：P(S)是一個(gè)一階謂詞公式，SST，即ST中任一元素S應(yīng)滿足的條件例2.例1中ADTStudentdata描述了對(duì)一個(gè)教師的評(píng)價(jià)：Inv_Studentdata≡Δmk_Studentdata(n,t)

Studentdata.n≠‘’t≠[]Inv_Choice≡ΔtChoice·lent=42/9/202352華東師大計(jì)算機(jī)科學(xué)技術(shù)系3、運(yùn)算功能規(guī)則運(yùn)算功能規(guī)則VDM形式規(guī)范中的主要形式，其一般形式為：OP（m1:Tm1,m2:Tm2,…mn:Tmn）r1:Tr1,…re,Treext PV1:Tv1…PVk:TvkpreC1 //C1表示為（mj,rk,)

postC2 //C2表示為（mj,Vi,rk,Vi)其中：OP是運(yùn)算名，mi是輸入?yún)⒘浚瑀i是輸出參量，ext表示Vi外部量；P{wr,rd}，表示可讀或可寫；pre是前置謂詞，post是后置謂詞。注：Vi是執(zhí)行OP前狀態(tài)值，Vi是執(zhí)行OP后狀態(tài)值。2/9/202353華東師大計(jì)算機(jī)科學(xué)技術(shù)系例3．簡(jiǎn)單計(jì)算器規(guī)范

reg:N //初始時(shí)外部變量reg=0LOAD(i:N)extwrreg:Npretruepostreg=iSHOW()r:Nextrdreg:N

pretruepostr=reg2/9/202354華東師大計(jì)算機(jī)科學(xué)技術(shù)系A(chǔ)DD(i:N)extwrreg:Npretruepostreg=reg+iDIVIDE(d:N)r:N

extwrreg:Npred≠0postd*r+reg=reg0≤reg<d2/9/202355華東師大計(jì)算機(jī)科學(xué)技術(shù)系為了描述方便，在前/后斷言中可以出現(xiàn)的一些結(jié)構(gòu)：⑴ let_inQ含義：在let后定義一些臨時(shí)變量，有效范圍是Q⑵ ifethenPelseQ 條件表達(dá)式⑶ 調(diào)用定義的函數(shù)，函數(shù)的規(guī)范為： 顯式定義：

f:p1:Tp1×p2:Tp2×…pn:TpnTrf(p1,…pn)≡…functionbody…其中：pi是f的參量，類型為Tpi，Tr為f的返回值2/9/202356華東師大計(jì)算機(jī)科學(xué)技術(shù)系隱式定義：f(p1:Tp1,p2:Tp2,…pn:Tpn)r:TrPre_f……Post_……其中：Pre是f的前置謂詞 Post是f的后置謂詞2/9/202357華東師大計(jì)算機(jī)科學(xué)技術(shù)系例4．一個(gè)分類運(yùn)算的VDM規(guī)范Index_entries=seqofNSORT(S:Index_entries)r:Index_entries extwroutput:Index_entries

pres≠[]postelemr=elemSis_sorted(r)

output=outputconj[r]其中：is_sorted(r)是一個(gè)函數(shù)，判斷自然數(shù)表是否已經(jīng)分類。2/9/202358華東師大計(jì)算機(jī)科學(xué)技術(shù)系三、VDM的程序正確性證明機(jī)制⑴關(guān)于函數(shù)的正確性證明f:P TPTr函數(shù)f滿足規(guī)范，當(dāng)且僅當(dāng)pTp，Pre_f(p)f(p)TrPost_f(p,f(p))⑵關(guān)于運(yùn)算的正確性證明設(shè)運(yùn)算op的規(guī)范為：……令表示所有狀態(tài)的集合，

=Tp×Tv1×……×Tv2×Tr證明機(jī)制為：Vpre_OP(V)rTr

Vpost_OP(V,V)其中：V=exec(OP,r)，即OP執(zhí)行后的狀態(tài)2/9/202359華東師大計(jì)算機(jī)科學(xué)技術(shù)系四、一個(gè)VDM規(guī)范的例子例5.用VDM為一個(gè)“教師職稱提升系統(tǒng)”書寫形式規(guī)范需求：該系統(tǒng)最終被定義為“Teacher-Promotion”的運(yùn)算。根據(jù)所要提升的名額（m）和全體教師的教學(xué)、科研評(píng)分表，選出總成績(jī)最好的前m名教師。并輸出教師的相關(guān)信息各運(yùn)算及其函數(shù)的意義 Get_persons: 取名額函數(shù) Teacher_order: 教師排序函數(shù) Score_sum: 教師積分計(jì)算函數(shù)Teacher_list_production: 教師序列生成函數(shù) Teaching_Research_score:評(píng)分科研數(shù)據(jù)采集函數(shù)

2/9/202360華東師大計(jì)算機(jī)科學(xué)技術(shù)系類型說明String=seqofchar Choice=seqofRTeacherSum=ComposeTeacherSumof Name2:String Total_score:R End Teacher_list=SeqofTeacherSum Studentdata_list=SeqofStudentdata Reseachdata_list=SeqofResearchdata注：其他的說明已在例1中給出2/9/202361華東師大計(jì)算機(jī)科學(xué)技術(shù)系類型不變式 Inv_studentdata≡mk_Studentdata(n,t) Studentdata.n≠‘’=>t≠[] Inv_Researchdata≡mk_Researchdata(n,r)

Researchdata.n≠‘’=>r≠[] Inv_choice≡tchoice.lent=42/9/202362華東師大計(jì)算機(jī)科學(xué)技術(shù)系函數(shù)及運(yùn)算Teacher_Promotion(tsl:Studentdata_list, rsl:Researchdata_list,m：N)P:Teacher_list extwroutput:Teacher_listPrelentsl=lenrsl∧ (tsl[i])=name1(rsl[i])/*教學(xué)、科研二個(gè)表中名字相同*/PostP=Get_Persons(Teacher_order (Teacher_list_production(ts1,rs1)),m)

∧output=outputconjP2/9/202363華東師大計(jì)算機(jī)科學(xué)技術(shù)系/*從已排序的教師序列表td中取出總成績(jī)最高的n位教師，從高到低次序放入tt表中*/

Get_Persons(td:Teacher_order_list,n:N) tt:Teacher_listPretd≠[]∧lentd≥n∧i,jindstdi<j=> total_score(td[i])≥total_score(td[j])Postlentt=n∧elemttelemtd∧i,jidnstti<j=>total_score(tt[i])>total_score(tt[j])∧xelemtt

yelemtd/elemtttotal_score(x)>total_score(y)2/9/202364華東師大計(jì)算機(jī)科學(xué)技術(shù)系/*將輸入的tl表中按總成績(jī)從高到低排序后放入另一個(gè)表d中*/Teacher_order(tl:Teacher_list)d:Teacher_listPre lentl>0Post elemd=elemtl∧i,jindsi<j =>total_sco