軟件工程形式化說明技術(shù)

軟件工程形式化說明技術(shù)CreativepurehandpaintedbusinesspresentationsCreativepurehandpaintedbusinesspresentations匯報(bào)人：視覺設(shè)計(jì)部門：創(chuàng)意設(shè)計(jì)部浪費(fèi)時(shí)間是一樁大罪過。---盧梭人生不可能一帆風(fēng)順，有成功，也有失?。挥虚_心，也有失落。如果我們把生活中的這些起起落落看得太重，那么生活對(duì)于我們來說永遠(yuǎn)都不會(huì)坦然，永遠(yuǎn)都沒有歡笑。人生應(yīng)該有所追求，但暫時(shí)得不到并不會(huì)阻礙日常生活的幸福，因此，擁有一顆平常心，是人生必不可少的潤(rùn)滑液劑?；氐阶顔渭兊某跣?，在最空的地方安坐，讓世界的吵鬧去喧囂它們自己吧！讓湖光山色去清秀它們自己吧！讓人群從遠(yuǎn)處走開或者自身邊擦過吧！普通人只想到如何度過時(shí)間，有才能的人設(shè)法利用時(shí)間。---德國(guó)哲學(xué)家叔本華我們總會(huì)長(zhǎng)大，會(huì)試著去成熟，會(huì)學(xué)著去放棄，去包容一些，即使過程艱難又漫長(zhǎng)，但要相信，天總會(huì)亮。軟件工程形式化說明技術(shù)軟件工程形式化說明技術(shù)CreativepurehandpaintedbusinesspresentationsCreativepurehandpaintedbusinesspresentations匯報(bào)人：視覺設(shè)計(jì)部門：創(chuàng)意設(shè)計(jì)部浪費(fèi)時(shí)間是一樁大罪過。---盧梭人生不可能一帆風(fēng)順，有成功，也有失敗；有開心，也有失落。如果我們把生活中的這些起起落落看得太重，那么生活對(duì)于我們來說永遠(yuǎn)都不會(huì)坦然，永遠(yuǎn)都沒有歡笑。人生應(yīng)該有所追求，但暫時(shí)得不到并不會(huì)阻礙日常生活的幸福，因此，擁有一顆平常心，是人生必不可少的潤(rùn)滑液劑?；氐阶顔渭兊某跣?，在最空的地方安坐，讓世界的吵鬧去喧囂它們自己吧！讓湖光山色去清秀它們自己吧！讓人群從遠(yuǎn)處走開或者自身邊擦過吧！普通人只想到如何度過時(shí)間，有才能的人設(shè)法利用時(shí)間。---德國(guó)哲學(xué)家叔本華我們總會(huì)長(zhǎng)大，會(huì)試著去成熟，會(huì)學(xué)著去放棄，去包容一些，即使過程艱難又漫長(zhǎng)，但要相信，天總會(huì)亮。關(guān)于形式化方法形式化方法是有爭(zhēng)議的。它們的支持者宣稱：它們可以引發(fā)軟件開發(fā)的革命。而批評(píng)者認(rèn)為：這是困難和不可能的。同時(shí)，對(duì)于大多數(shù)人來說，對(duì)形式化方法是如此不熟悉，以至難于判斷這些爭(zhēng)論。2形式化的程序非形式化方法：自然語言描述半形式化方法（欠形式化方法）：數(shù)據(jù)流圖、實(shí)體-聯(lián)系圖形式化方法：一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)3非形式化方法的缺點(diǎn)二義性：操作員名和口令可能存在矛盾：監(jiān)控溫度/往往距離很遠(yuǎn)含糊性：由雷達(dá)操作員使用的系統(tǒng)界面應(yīng)該是用戶友好的不完整性：傳感器抽象層次混亂：系統(tǒng)的目的是跟蹤倉(cāng)庫(kù)中的庫(kù)存/當(dāng)?shù)陠T輸入命令withdraw及參數(shù)，系統(tǒng)將回饋是否允許移去貨物4形式化方法的優(yōu)點(diǎn)簡(jiǎn)潔幾乎可以沒有二義性可以通過數(shù)學(xué)方法來發(fā)現(xiàn)矛盾和不完整性在不同軟件工程活動(dòng)之間平滑地過渡提供了高層確認(rèn)的手段5有窮狀態(tài)機(jī)有窮狀態(tài)機(jī)：可以準(zhǔn)確的描述一個(gè)系統(tǒng)6有窮狀態(tài)機(jī)有窮狀態(tài)機(jī)的組成部分（五元組）狀態(tài)集輸入集轉(zhuǎn)換函數(shù)初始態(tài)終態(tài)集7有窮狀態(tài)機(jī)謂詞：全局狀態(tài)的函數(shù)“貓是動(dòng)物”一句中的“是動(dòng)物”就是一個(gè)謂詞，而“貓”是客體“3大于2”中“大于”是一個(gè)謂詞轉(zhuǎn)換規(guī)則：當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]=>下個(gè)狀態(tài)當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]+謂詞=>下個(gè)狀態(tài)8有窮狀態(tài)機(jī)電梯系統(tǒng)的描述9有窮狀態(tài)機(jī)10有窮狀態(tài)機(jī)便于書寫，驗(yàn)證可以通過CASE工具將有窮狀態(tài)機(jī)的規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a開發(fā)一個(gè)規(guī)模比較大的系統(tǒng)時(shí)，三元組數(shù)量太多沒有處理定時(shí)需求11Petri網(wǎng)Petri網(wǎng)：最初用于自動(dòng)化處理方面，后來才用于計(jì)算機(jī)科學(xué)中位置：用圓圈表示轉(zhuǎn)換：用短直線表示用于轉(zhuǎn)換的輸入函數(shù)：由位置指向轉(zhuǎn)換的箭頭表示用于轉(zhuǎn)換的輸出函數(shù)：由轉(zhuǎn)換指向位置的箭頭表示12Petri網(wǎng)權(quán)標(biāo)（Token）及權(quán)標(biāo)的表示帶權(quán)標(biāo)的Petri網(wǎng)：是否允許轉(zhuǎn)換禁止線：帶小圓圈的輸入線表示帶禁止線的Petri網(wǎng)13Petri網(wǎng)14Petri網(wǎng)15有窮狀態(tài)機(jī)便于書寫，驗(yàn)證可以通過CASE工具將有窮狀態(tài)機(jī)的規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a開發(fā)一個(gè)規(guī)模比較大的系統(tǒng)時(shí)，三元組數(shù)量太多沒有處理定時(shí)需求11Petri網(wǎng)Petri網(wǎng)：最初用于自動(dòng)化處理方面，后來才用于計(jì)算機(jī)科學(xué)中位置：用圓圈表示轉(zhuǎn)換：用短直線表示用于轉(zhuǎn)換的輸入函數(shù)：由位置指向轉(zhuǎn)換的箭頭表示用于轉(zhuǎn)換的輸出函數(shù)：由轉(zhuǎn)換指向位置的箭頭表示12Petri網(wǎng)權(quán)標(biāo)（Token）及權(quán)標(biāo)的表示帶權(quán)標(biāo)的Petri網(wǎng)：是否允許轉(zhuǎn)換禁止線：帶小圓圈的輸入線表示帶禁止線的Petri網(wǎng)13Petri網(wǎng)14Petri網(wǎng)15Z語言Z語言包含的內(nèi)容：給定的集合、數(shù)據(jù)類型及常數(shù)狀態(tài)定義初始狀態(tài)操作16Z語言給定的集合：用[]表示狀態(tài)定義：格（schema）初始狀態(tài)操作：？表示輸入變量，！表示輸出變量，′表示某個(gè)變量的值發(fā)生了改變，＼表示差運(yùn)算17Z語言18Z語言19Z語言20Z語言塊處理21Z語言22Z語言23Z語言24Z語言用Z語言書寫的規(guī)格說明，比較容易發(fā)現(xiàn)錯(cuò)誤減少了模糊性、不一致性和遺漏可以嚴(yán)格驗(yàn)證規(guī)格說明的正確性雖然完全掌握Z語言困難，但是學(xué)會(huì)編寫還是比較容易的使用Z語言可以降低軟件開發(fā)費(fèi)用和總時(shí)間從Z語言的規(guī)格說明轉(zhuǎn)換出自然語言的規(guī)格說明更為清晰25應(yīng)用形式化方法的準(zhǔn)則應(yīng)該選用適當(dāng)?shù)谋硎痉椒☉?yīng)該形式化，但不要過分形式化應(yīng)該估算成本應(yīng)該有形式化方法顧問隨時(shí)提供咨詢不應(yīng)該放棄傳統(tǒng)的開發(fā)方法應(yīng)該建立詳盡的文檔不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)不應(yīng)該盲目依賴形式化方法應(yīng)該測(cè)試、測(cè)試再測(cè)試應(yīng)該重用2