J.Woodcock&J.Davies_UsingZ_1996_C1 閱讀
文章概要
隨著軟件的日益發(fā)展, 軟件的功能等需求越來(lái)越多, 文檔也隨之增加, 組件之間的交互和沖突最后導(dǎo)致系統(tǒng)出現(xiàn)問(wèn)題, 逐漸偏離了我們的預(yù)期. 為解決該問(wèn)題, 其中一個(gè)重要的方法就是形式化.
雖然在軟件生命周期之中, 我們有許多文檔, 涵蓋大量的圖片, 文字和圖表, 但是這些都是模糊不清的, 重要的信息都被隱藏在不相干的細(xì)節(jié)之中, 缺陷發(fā)現(xiàn)的過(guò)于遲, 進(jìn)而導(dǎo)致嚴(yán)重的問(wèn)題. 形式化解決了該問(wèn)題, 它可以產(chǎn)出精確的, 非模糊的文檔, 并且該文檔可以用于設(shè)計(jì)階段, 以及作為后續(xù)的開(kāi)發(fā), 測(cè)試和維護(hù)作為導(dǎo)向.
雖然形式化十分有用, 但是其數(shù)學(xué)基礎(chǔ)是和通常的數(shù)學(xué)不太一樣的, 因此使用它的成本是較為高昂的, 但是不可否認(rèn)的是, 形式化的的確確可以減少最終的耗費(fèi).
CICS是世界上大多數(shù)成功的軟件之中的一個(gè), 它是一個(gè)信息管理系統(tǒng), 并且被廣泛地使用在各個(gè)領(lǐng)域, 開(kāi)發(fā)之后的10年, 軟件變得十分復(fù)雜, 提出來(lái)一個(gè)解決方案是, 找到一個(gè)更為精確的方法來(lái)確定功能, 而這樣的精確就需要使用數(shù)學(xué)技術(shù). Kenny和Hoare嘗試解決這個(gè)問(wèn)題, 引出了Z符號(hào), 利用該方法來(lái)對(duì)CICS確定新的功能, 這種方法易于學(xué)習(xí)和使用, 即使使用者沒(méi)有任何數(shù)學(xué)的預(yù)備知識(shí).
Z notation是基于集合論和數(shù)學(xué)邏輯的, Z notation使得其數(shù)學(xué)形式是結(jié)構(gòu)化的, 由聲明和約束構(gòu)成的模式, 這樣的語(yǔ)言可以用來(lái)表述一個(gè)系統(tǒng)的狀態(tài), 屬性等, 重要的是, 可以用該方法來(lái)改良原有的設(shè)計(jì). 另外, Z notation使用自然語(yǔ)言進(jìn)行表述, 對(duì)于讀者來(lái)說(shuō)閱讀起來(lái)十分輕松. 數(shù)學(xué)語(yǔ)言加上強(qiáng)大的結(jié)構(gòu)化技術(shù), 最終可以產(chǎn)出形式化的規(guī)格說(shuō)明書(shū), 可以使用數(shù)學(xué)邏輯的驗(yàn)證技術(shù)來(lái)對(duì)這些說(shuō)明書(shū)進(jìn)行推斷. Z并不是用于非功能屬性的描述, 比如可用性, 大小, 性能和可依靠性.
構(gòu)造證明的過(guò)程可以幫助我們更好地理解系統(tǒng)的需求, 幫助我們找到那些隱藏的假設(shè), 在規(guī)格說(shuō)明書(shū)上的證明對(duì)于軟件質(zhì)量來(lái)說(shuō)至關(guān)重要.
閱讀感悟
該文章很好地梳理了Z notation的起源. 從軟件的開(kāi)發(fā)談起, 引用CICS的開(kāi)發(fā)歷程, 引出了Z notation, 闡述了Z notation的各方面的優(yōu)點(diǎn)以及其特有的性質(zhì), 又說(shuō)明了在Z notation之中Proof的重要性, 給出其主要的功能和貢獻(xiàn), 隨后用了一個(gè)經(jīng)典的抽象化, 表現(xiàn)出了形式化和非形式化的區(qū)別, 形象地顯示了形式化的優(yōu)勢(shì)以及可讀性.
