Z規(guī)格說(shuō)明自動(dòng)生成器①

趙正旭,溫晉杰(石家莊鐵道大學(xué),石家莊 050043)(石家莊鐵道大學(xué) 信息科學(xué)與技術(shù)學(xué)院,石家莊 050043)

?

Z規(guī)格說(shuō)明自動(dòng)生成器①

趙正旭1,溫晉杰2
1(石家莊鐵道大學(xué),石家莊 050043)
2(石家莊鐵道大學(xué) 信息科學(xué)與技術(shù)學(xué)院,石家莊 050043)

摘 要:形式化Z語(yǔ)言采用嚴(yán)格的數(shù)學(xué)理論可以有效提高軟件的可靠性和魯棒性,但是由于其包含的數(shù)學(xué)理論使得只有少數(shù)人能夠熟練應(yīng)用Z語(yǔ)言進(jìn)行形式化規(guī)格說(shuō)明書的編寫.目前,多數(shù)對(duì)于Z語(yǔ)言的研究集中在理論階段,還沒(méi)有相應(yīng)的工具支持Z規(guī)格說(shuō)明的自動(dòng)生成.本文中對(duì)于Z規(guī)格說(shuō)明自動(dòng)生成器的研究有助于降低Z規(guī)格說(shuō)明書的編寫難度,降低了形式化開發(fā)的難度及成本,對(duì)于形式化Z語(yǔ)言的推廣具有重要的意義.

關(guān)鍵詞:Z語(yǔ)言; 形式化; 自動(dòng)生成器; 規(guī)約; 語(yǔ)義分析

形式化Z語(yǔ)言是一種基于一階謂詞邏輯和集合論的規(guī)格說(shuō)明語(yǔ)言[1].可以進(jìn)行計(jì)算機(jī)硬件以及軟件系統(tǒng)的描述與驗(yàn)證,尤其適合于極重大安全性系統(tǒng),如航空航天項(xiàng)目.其基本思想是利用一些已知特性的數(shù)學(xué)抽象來(lái)為目標(biāo)軟件系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型[2].在需求規(guī)格說(shuō)明中,Z語(yǔ)言精確的描述軟件系統(tǒng)“做什么”而不涉及“怎么做”,只對(duì)目標(biāo)軟件系統(tǒng)進(jìn)行功能描述.通過(guò)明確定義狀態(tài)和操作來(lái)建立一個(gè)系統(tǒng)模型(使系統(tǒng)從一個(gè)狀態(tài)轉(zhuǎn)換到另一個(gè)狀態(tài)),具有其他描述方法不可比擬的嚴(yán)謹(jǐn)性、清晰性和無(wú)二義性[2].但是,從國(guó)內(nèi)的現(xiàn)狀來(lái)看,形式化Z語(yǔ)言的應(yīng)用還有待于進(jìn)一步的推廣和深入,降低形式化開發(fā)的成本是一個(gè)重要前提.利用形式化方法Z語(yǔ)言軟件開發(fā)的成本高居不下的一個(gè)重要原因就在于Z語(yǔ)言需求規(guī)格說(shuō)明書的撰寫環(huán)節(jié).Z需求規(guī)格說(shuō)明書的撰寫要求撰寫者對(duì)數(shù)學(xué)理論熟練掌握,包括數(shù)據(jù)結(jié)構(gòu)、數(shù)學(xué)抽象思維、數(shù)學(xué)建模等都有一定的要求,如果對(duì)Z語(yǔ)言沒(méi)有任何的了解或者接觸,想要撰寫一份合格的Z規(guī)格說(shuō)明書既消耗時(shí)間又消耗物力財(cái)力,具有相當(dāng)高的難度,很大程度上影響了Z語(yǔ)言的推廣.主要有以下兩種原因:

(1)Z語(yǔ)言包含的數(shù)學(xué)符號(hào)和邏輯操作對(duì)于軟件工程領(lǐng)域的技術(shù)人員來(lái)說(shuō),是及其陌生和難以理解的.學(xué)習(xí)和使用Z語(yǔ)言是一個(gè)十分困難的過(guò)程.

(2)軟件設(shè)計(jì)師和軟件工程師對(duì)形式化方法的作用有不同的認(rèn)識(shí),而對(duì)Z語(yǔ)言形式化描述中的數(shù)學(xué)理論缺乏興趣.

所以,一套具有良好用戶界面、易于學(xué)習(xí)和操作簡(jiǎn)單的Z語(yǔ)言支撐工具,對(duì)于形式化Z語(yǔ)言的推廣應(yīng)用是大有裨益的.Z語(yǔ)言作為目前使用最為廣泛的形式化描述語(yǔ)言之一,它有以下幾個(gè)主要特點(diǎn):

首先,Z語(yǔ)言不是計(jì)算機(jī)程序編制工具或編程系統(tǒng).Z語(yǔ)言是設(shè)計(jì)規(guī)范,采用了包括集合、序列、包、關(guān)系、函數(shù)、類型、對(duì)象等抽象的數(shù)學(xué)理論.所以,Z語(yǔ)言是一種數(shù)學(xué)語(yǔ)言.其次,Z語(yǔ)言形成的規(guī)格說(shuō)明的形式不是完全類似于ASCII碼的文字和字符串,而是包括了規(guī)范化的數(shù)學(xué)符號(hào)和演算圖形.Z語(yǔ)言形成的規(guī)格說(shuō)明的內(nèi)容不是能編譯和運(yùn)行的程序編碼,而是用來(lái)進(jìn)行邏輯推理和數(shù)學(xué)演算的.另外,Z語(yǔ)言沒(méi)有完全使用數(shù)學(xué)符號(hào)來(lái)形成規(guī)格說(shuō)明,它也使用了自然語(yǔ)言來(lái)定義變量和添加批注.所以,由Z語(yǔ)言生成的規(guī)格說(shuō)明易于讀寫和解析.最后,由Z語(yǔ)言所形成的規(guī)格說(shuō)明不僅嚴(yán)謹(jǐn)、清晰、無(wú)二義,而且可以通過(guò)形式化方法軟件對(duì)其進(jìn)行驗(yàn)證和推理.

1　主要的Z語(yǔ)言編輯工具

一直以來(lái),軟件開發(fā)者都期望研發(fā)出的軟件具有較高的可行性和魯棒性,形式化方法使用適當(dāng)?shù)臄?shù)學(xué)分析以提高設(shè)計(jì)的可靠性和魯棒性.但是,由于采用形式化方法的成本高意味著它們通常只用于開發(fā)注重安全性的高度整合的系統(tǒng).所以,對(duì)Z語(yǔ)言輔助工具的研究以降低形式化開發(fā)的成本就成為一個(gè)研究的熱點(diǎn).針對(duì)Z語(yǔ)言的輔助工具有很多種,但是大多數(shù)都不支持于2002年頒布的Z語(yǔ)言ISO標(biāo)準(zhǔn),關(guān)于Z語(yǔ)言的工具在文獻(xiàn)報(bào)告中并不多見,主流的Z語(yǔ)言支撐工具可以分為Z獨(dú)立系統(tǒng)、Z接口模塊、Z集成插件.Z獨(dú)立系統(tǒng)中具有代表性的為“ZEVES”和 “Community Z Tools”簡(jiǎn)稱“CZT”; Z接口模塊中具有代表性的工具為“Z2HTML”; Z集成插件中具有代表意義的為“Z Word Tools”; 接下來(lái),重點(diǎn)介紹一下使用最為廣泛的“Z Word Tools”.

“Z Word Tools”是基于Microsoft Office Word的Z語(yǔ)言的插件,在計(jì)算機(jī)上安裝“Z Word Tools”后,可以在Microsoft Office Word中進(jìn)行Z語(yǔ)言的編輯、類型檢查、文檔結(jié)構(gòu)檢查等工作,輸出的是word文檔,只有自己的計(jì)算機(jī)上面裝有“Z Word Tools”才可以正確地查看該文檔.“Z Word Tools”具體功能包括:

(1)向微軟Office Word提供了了一個(gè)Z語(yǔ)言的Unicode字形庫(kù)[16];

(2)具有Z語(yǔ)言的“所見即所得”風(fēng)格的人機(jī)交互編輯界面并集成在微軟Office Word系統(tǒng)中;

(3)拼寫檢查使用了模糊的Spivey Z[17]和ISO標(biāo)準(zhǔn)Z[18,19]以及CZT功能;

(4)可以在Z語(yǔ)言規(guī)格說(shuō)明中設(shè)置索引和交叉索引;

(5)為Z語(yǔ)言規(guī)格說(shuō)明繪制與顯示結(jié)構(gòu)示意圖.

通過(guò)集成插件系統(tǒng)來(lái)實(shí)現(xiàn)Z語(yǔ)言形式描述克服了上述獨(dú)立系統(tǒng)的困難,因此提高了Z語(yǔ)言形式描述的規(guī)格說(shuō)明的兼容性,從而擴(kuò)展了Z語(yǔ)言的應(yīng)用范圍.

圖1　Z Word Tools菜單欄

嚴(yán)格來(lái)講,上述主流的Z語(yǔ)言輔助工具屬于Z語(yǔ)言的編輯器,本文將要介紹的是Z規(guī)格說(shuō)明自動(dòng)生成器.與上述Z語(yǔ)言輔助工具相比,我們的Z規(guī)格說(shuō)明自動(dòng)生成器具有以下五個(gè)特點(diǎn):

(1)Z規(guī)格說(shuō)明自動(dòng)生成器完全是自主研發(fā).Z規(guī)格說(shuō)明自動(dòng)生成器的菜單欄、提示信息、工具欄均為漢語(yǔ),它們通俗易懂并且便于軟件工程和技術(shù)人員學(xué)習(xí)和使用Z語(yǔ)言.

(2)Z規(guī)格說(shuō)明自動(dòng)生成器是一個(gè)獨(dú)立系統(tǒng),它不需要和任何其它應(yīng)用程序集成使用.

(3)Z規(guī)格說(shuō)明自動(dòng)生成器的每一步輸入過(guò)程都非常簡(jiǎn)單.它是通過(guò)人機(jī)交互的圖形界面并且按有序的步驟進(jìn)行選項(xiàng)式輸入.所以,Z規(guī)格說(shuō)明自動(dòng)生成器的操作方便并且Z語(yǔ)言形式化的描述的過(guò)程容易被軟件工程和技術(shù)人員所理解.

(4)Z規(guī)格說(shuō)明自動(dòng)生成器改變了Z語(yǔ)言的使用方法.它不需要軟件工程和技術(shù)人員熟悉和理解Z語(yǔ)言的抽象演算以及基礎(chǔ)概念和數(shù)學(xué)理論,它只需要軟件工程和技術(shù)人員理解狀態(tài)變量的類型,例如哪個(gè)是屬于全局變量,哪個(gè)是屬于輸出變量,哪個(gè)是屬于輸入變量.

(5)由Z規(guī)格說(shuō)明自動(dòng)生成器定義并生成的Z模式與標(biāo)準(zhǔn)的Z模式一致,并且以圖像文件存儲(chǔ),便于傳播.

Z語(yǔ)言實(shí)際上是一種數(shù)學(xué)表達(dá)規(guī)范,而Z規(guī)范中的基礎(chǔ)理論和概念對(duì)于軟件工程領(lǐng)域的技術(shù)人員來(lái)說(shuō),是極其陌生和難以理解的.學(xué)習(xí)和使用Z語(yǔ)言是一個(gè)十分困難的過(guò)程,這可能就是Z語(yǔ)言沒(méi)有得到廣泛使用和如期發(fā)揮它作用的主要原因.本節(jié)介紹了Z語(yǔ)言相關(guān)的一些常用輔助工具,從這些系統(tǒng)的結(jié)構(gòu)方面論述了Z語(yǔ)言的使用方法.這些實(shí)用方法無(wú)疑是今后研究和探討如何進(jìn)一步推廣和使用Z語(yǔ)言的關(guān)鍵和焦點(diǎn).

目前,幾乎所有的與Z語(yǔ)言相關(guān)的形式化描述系統(tǒng)都是注重于Z語(yǔ)言的撰寫、編輯、檢查、驗(yàn)證等過(guò)程.這些系統(tǒng)并沒(méi)有使軟件工程和技術(shù)人員從Z語(yǔ)言的基礎(chǔ)概念和數(shù)學(xué)理論中完全解脫出來(lái).在今后的實(shí)際應(yīng)用中,Z語(yǔ)言應(yīng)該側(cè)重于方便易懂的用戶界面、易于學(xué)習(xí)和操作簡(jiǎn)單的形式化方法的輔助工具.在下文將介紹一個(gè)自己編碼完成的Z規(guī)格說(shuō)明自動(dòng)生成器.希望這個(gè)自動(dòng)生成器能夠?yàn)檐浖こ毯图夹g(shù)人員屏蔽Z語(yǔ)言的基礎(chǔ)概念和數(shù)學(xué)理論,幫助他們順利完成Z語(yǔ)言形式化描述的規(guī)格說(shuō)明的撰寫任務(wù).這對(duì)促進(jìn)Z語(yǔ)言的應(yīng)用推廣十分重要.

2　設(shè)計(jì)與實(shí)現(xiàn)

Z規(guī)格說(shuō)明自動(dòng)生成器的設(shè)計(jì)宗旨是要面向所有軟件過(guò)程參與者的,并不只是面向Z語(yǔ)言的學(xué)習(xí)者.每一名用戶利用該自動(dòng)生成器都可以很方便地生成一份垂直模式的Z規(guī)格說(shuō)明.

Z規(guī)格說(shuō)明自動(dòng)生成器的界面有兩個(gè)區(qū)域,即輸入?yún)^(qū)域和顯示區(qū)域,輸入?yún)^(qū)域又分為狀態(tài)變量的輸入?yún)^(qū)和變量之間操作關(guān)系的輸入?yún)^(qū)域.如圖2所示.

圖2　Z規(guī)格說(shuō)明自動(dòng)生成器首頁(yè)

在狀態(tài)變量的輸入?yún)^(qū)內(nèi)可以輸入的內(nèi)容有以下幾個(gè)類型.

模式類型: Z語(yǔ)言的模式一共有四種類型.它們分別為初始化模式、狀態(tài)模式、操作模式、報(bào)錯(cuò)模式.當(dāng)我們點(diǎn)擊下拉框時(shí),下拉框里便會(huì)顯示出這四種模式類型,以供我們選擇.如圖3所示.

圖3　模式類型示意圖

涉及模式: 涉及模式也是關(guān)聯(lián)模式,它表示的是當(dāng)前模式中所要包含的模式.例如,假如我們要描述一個(gè)軟件系統(tǒng)的密碼修改操作,我們必須要求該用戶成功登錄該系統(tǒng),所以描述修改密碼的Z模式中就要包含描述成功登錄系統(tǒng)的Z模式.描述成功登錄系統(tǒng)的Z模式就是描述修改密碼的Z模式的涉及模式.

模式名稱: 用于輸入用戶自行定義的模式名稱.

變量種類: 主要是為了區(qū)分所定義的變量是屬于哪一種變量.我們一共有三種變量,即全局變量、輸出變量、輸入變量.如圖4所示.

圖4　變量種類示意圖

變量名稱: 選擇變量種類之后,我們?cè)诳删庉嬢斎肟蛑休斎胂鄳?yīng)的自定義變量名稱.

變量類型: 輸入變量名稱所屬于的類型,可以自定義變量類型.比如,數(shù)字2屬于自然數(shù)?.

在變量類型一欄的后面有一個(gè)“+”按鈕,我們可以根據(jù)模式中變量的數(shù)目來(lái)動(dòng)態(tài)地添加“變量種類”,“變量名稱”,“變量類型”的輸入框.

操作關(guān)系就是上面所輸入的狀態(tài)變量之間的對(duì)應(yīng)關(guān)系.因?yàn)閆語(yǔ)言采用了非ASCII符號(hào)來(lái)表示變量之間關(guān)系,所以自動(dòng)生成器采用了Unicode編碼符號(hào)來(lái)處理和顯示這些特殊的Z語(yǔ)言符號(hào).我們點(diǎn)擊輸入?yún)^(qū)域的下拉框之后,自動(dòng)生成器就會(huì)顯示出一系列的表示集合與集合或者是變量與變量之間關(guān)系的特殊符號(hào)含義以供我們選擇.

顯示區(qū)域要根據(jù)輸入?yún)^(qū)域所輸入的信息顯示相應(yīng)的Z模式框.

在Z規(guī)格說(shuō)明自動(dòng)生成器具體實(shí)施的過(guò)程中,主要遇到以下三個(gè)問(wèn)題:

①Z模式框的顯示

Z模式框是Z規(guī)格說(shuō)明中的基本結(jié)構(gòu),首先面臨的問(wèn)題就是如何以圖形化的方式顯示Z模式框.經(jīng)過(guò)分析,Z模式框是由水平線與豎直線組成,在構(gòu)造Z模式框的時(shí)候,可以利用水平線和垂直線拼接而成.顯示Z模式框水平線和垂直線的主要代碼如下所示:

②顯示區(qū)域的保存

顯示區(qū)域顯示最終生成的Z規(guī)約,為了降低保存的難度,采取的方案是將輸出結(jié)果顯示在panel控件上,panel控件主要是作為其他控件的容器,我們可以根據(jù)需求設(shè)置其的可見性.將panel區(qū)域的內(nèi)容保存為圖片時(shí),需要獲取panel控件的源點(diǎn)坐標(biāo)以及panel區(qū)域的長(zhǎng)寬通過(guò)屏幕捕捉函數(shù)截取屏幕按照指定的文件路徑保存到相應(yīng)的文件夾當(dāng)中.核心代碼如下所示:

我們把自動(dòng)生成器的輸出采用.jpg圖像文件來(lái)保存,這是因?yàn)槿齻€(gè)方面的因素.首先是為了避免對(duì)Z語(yǔ)言的特殊符號(hào)和非ASCII符號(hào)的預(yù)處理.其次是因?yàn)?jpg圖像文件的讀取和顯示不需要在計(jì)算機(jī)上安裝專用Z語(yǔ)言形式描述軟件工具,如CZT或微軟Office Word與Z Word Tools的集成輔助工具.最后是考慮.jpg圖像文件便于網(wǎng)絡(luò)傳輸并且可以方便地嵌入網(wǎng)頁(yè)和常用的文字文檔之中.但是,輸出的.jpg圖像文件不能支持Z語(yǔ)言規(guī)格說(shuō)明的自動(dòng)檢查,也不能支持軟件工程中對(duì)軟件設(shè)計(jì)的自動(dòng)檢驗(yàn)和驗(yàn)證.

③特殊符號(hào)的顯示

Z語(yǔ)言中包含為數(shù)眾多的特殊符號(hào),經(jīng)過(guò)仔細(xì)的考察,至今,沒(méi)有任何一種字體能夠?qū)語(yǔ)言中的特殊符號(hào)全部包含其中,所以,我們采用Unicode編碼來(lái)實(shí)現(xiàn).Unicode碼是一種國(guó)際標(biāo)準(zhǔn)編碼,擴(kuò)展自ASCII字元集.電腦上普遍使用的每字元有8位元寬; 而Unicode使用全16位元字元集.這使得Unicode能夠表示世界上所有的書寫語(yǔ)言中可能用于電腦通訊的字元、象形文字和其他符號(hào).

為了更進(jìn)一步簡(jiǎn)化該生成器的使用,在前臺(tái)界面不會(huì)出現(xiàn)Z語(yǔ)言中繁雜的特殊符號(hào),出現(xiàn)的均為特殊符號(hào)對(duì)應(yīng)的具體含義,例如“∧”對(duì)應(yīng)為“合取”、“?”對(duì)應(yīng)為“空集”等.用戶選擇特殊符號(hào)對(duì)應(yīng)的含義后,我們就可以判斷用戶選擇的是哪個(gè)特殊符號(hào),然后在Z規(guī)格說(shuō)明中的相應(yīng)位置插入該符號(hào)對(duì)應(yīng)的Unicode碼,然后根據(jù)Unicode編碼將該特殊符號(hào)的符號(hào)形狀顯示在panel區(qū)域的相應(yīng)位置[3].如圖5所示.

圖5　顯示原理示意圖

表1是Z語(yǔ)言中部分特殊符號(hào)與Unicode編碼以及特殊符號(hào)與其具體含義三者的相互映射關(guān)系,由于篇幅有限,沒(méi)有將所有特殊符號(hào)與Unicode碼的映射給出.

表1　特殊符號(hào)Unicode編碼表

另外,為了規(guī)范Z規(guī)格說(shuō)明的生成,還需要基本定義以下規(guī)則:

規(guī)則1.在模式類型下拉框中,用戶選擇初始化模式時(shí),不包含任何已定義的狀態(tài)模式與操作模式,所以涉及模式為空; 用戶選擇模式類型為錯(cuò)誤模式時(shí),由于,錯(cuò)誤模式描述操作操作錯(cuò)誤時(shí)的狀態(tài)量的變化及對(duì)應(yīng)關(guān)系,操作失敗不引起狀態(tài)量的變化,對(duì)其所涉及模式進(jìn)行修飾的時(shí)候選擇符號(hào)“Ξ”描述,其余情況均會(huì)引起狀態(tài)量的變化,選擇符號(hào)“Δ”來(lái)描述; 其中,ΔSys? [Sys,Sys′]和ΞSys? [ΔSys|θSys=θSys′]

規(guī)則2.用戶在變量種類下拉框選著為輸入變量時(shí),在顯示區(qū)域后面緊跟“?”進(jìn)行修飾; 如果選擇,輸出變量時(shí),在顯示區(qū)域后面緊跟“!”進(jìn)行修飾; 選擇為全局變量時(shí),如果該全局變量表示的是一個(gè)集合,則其所屬類型前面加“IP”,表示是該集合冪集的一個(gè)子集;如果該狀態(tài)變量表示的是一個(gè)有限集合,則其所屬類型前面加“IF”,表示是該集合冪集的一個(gè)有限子集;否則不進(jìn)行修飾.

上述兩條規(guī)則針對(duì)用戶的不同選擇而定義,基本能夠完成簡(jiǎn)單的Z規(guī)格說(shuō)明的生成.但是,本規(guī)格說(shuō)明自動(dòng)生成器尚處于研發(fā)應(yīng)用的初期,考慮還不夠周全,定義的規(guī)則也比較粗糙,功能還有待于進(jìn)一步的增加完善.

3　實(shí)例研究與工具演示

手機(jī)是我們?nèi)粘Ｉ钪斜夭豢缮俚耐ㄓ嵐ぞ?本節(jié)選擇聯(lián)系人相關(guān)操作進(jìn)行Z語(yǔ)言的描述與驗(yàn)證.

首先我們要確定手機(jī)通訊錄要涉及到的狀態(tài)變量并對(duì)其命名.通訊錄中聯(lián)系人姓名為PhoneName、通訊錄中聯(lián)系人電話定義為PhoneNumber,定義姓名和電話號(hào)碼的類型分別為Name與Number.接下來(lái),我們要定義操作之后系統(tǒng)要給出的提示信息.由于操作之后系統(tǒng)要給出的提示信息為具體值,且比較簡(jiǎn)單,所以我們可以通過(guò)枚舉法來(lái)定義,枚舉如下:

RESPONSE::= Success.

描述任何一個(gè)客觀事物,首先就是對(duì)其進(jìn)行初始化,包括對(duì)涉及到的狀態(tài)變量、集合的初始化,使用Z語(yǔ)言的插件“Z Word Tools”在Microsoft Office Word中編輯初始化模式如下.

為了驗(yàn)證本課題組開發(fā)的Z規(guī)格說(shuō)明自動(dòng)生成器的可行性,利用Z規(guī)格說(shuō)明自動(dòng)生成器生成Z模式的時(shí)候,選擇、輸入以及結(jié)果的輸出顯示如圖6所示.

圖6　初始化模式生成界面

增加聯(lián)系人操作會(huì)涉及到初始化的變量,所以要涉及初始化模式InitPhone,增加聯(lián)系人成功之后,通訊錄中聯(lián)系人姓名為PhoneName會(huì)改變、通訊錄中聯(lián)系人電話PhoneNumber也會(huì)變?yōu)樵械奶?hào)碼的集合加上新輸入的聯(lián)系人電話,Z模式描述如下:

利用Z規(guī)格說(shuō)明自動(dòng)生成器生成Z模式的時(shí)候,選擇以及輸入的數(shù)據(jù)如圖7所示:

圖7　增加聯(lián)系人輸出界面

當(dāng)我們要?jiǎng)h除聯(lián)系人時(shí),我們一般按照這樣的操作流程進(jìn)行,即輸入要?jiǎng)h除的聯(lián)系人的姓名,然后將對(duì)應(yīng)的聯(lián)系人信息及其電話號(hào)碼一起刪除.在這個(gè)操作中,姓名與電話號(hào)碼滿足二元對(duì)應(yīng)關(guān)系.借助于這種對(duì)應(yīng)關(guān)系,我們可以方便地通過(guò)所輸入的姓名來(lái)找到相對(duì)應(yīng)的電話號(hào)碼.要?jiǎng)h除聯(lián)系人的操作的Z語(yǔ)言描述如下:

我們利用Z規(guī)格說(shuō)明自動(dòng)生成器所生成的Z模式Deletesuccess以及所做的選擇和輸入的數(shù)據(jù)如圖8所示.

Z規(guī)格說(shuō)明自動(dòng)生成器的顯示區(qū)域所顯示的輸出結(jié)果如圖9所示.當(dāng)我們完成要?jiǎng)h除聯(lián)系人操作的描述時(shí),通過(guò)點(diǎn)擊保存按鈕,模式Deletesuccess以圖像格式保存為磁盤文件.

圖8　刪除聯(lián)系人輸入界面

圖9　刪除聯(lián)系人生成圖

修改聯(lián)系人的操作一般是針對(duì)該聯(lián)系人的電話號(hào)碼的修改.描述這個(gè)與前面描述的刪除聯(lián)系人的操作類似,它們都是借助于聯(lián)系人的姓名與電話號(hào)碼之間的對(duì)應(yīng)關(guān)系進(jìn)行的.我們通過(guò)輸入聯(lián)系人的姓名來(lái)找到相對(duì)應(yīng)的電話號(hào)碼,然后來(lái)進(jìn)行修改操作.描述這個(gè)操作的Z模式如下:

圖10所示的截屏是我們利用Z規(guī)格說(shuō)明自動(dòng)生成器生成的描述修改聯(lián)系人的操作的Z模式Modifysuccess的選擇以及輸入的數(shù)據(jù).

圖11所顯示是Z規(guī)格說(shuō)明自動(dòng)生成器輸出區(qū)域顯示并最終所生成的Modifysuccess模式以圖像格式保存到磁盤文件里.

上述實(shí)例介紹和驗(yàn)證了Z規(guī)格說(shuō)明自動(dòng)生成器的功能性和可用性,通過(guò)對(duì)一個(gè)實(shí)際應(yīng)用程序的Z語(yǔ)言描述,敘述了Z語(yǔ)言的一種新的使用方法.借助于形式化描述的輔助工具,使軟件工程和技術(shù)人員能夠在不熟悉Z語(yǔ)言的基礎(chǔ)概念和數(shù)學(xué)理論的情況下使用Z語(yǔ)言來(lái)撰寫正確的Z規(guī)格說(shuō)明書.實(shí)踐證明,該規(guī)格說(shuō)明自動(dòng)生成器可以有效地生成BOX風(fēng)格的Z規(guī)格說(shuō)明,而且具有很好的可行性.本項(xiàng)研究是對(duì)于Z規(guī)格說(shuō)明的自動(dòng)生成的一次有效嘗試,為Z規(guī)格說(shuō)明自動(dòng)生成器的研究起了帶頭作用.

圖10　修改聯(lián)系人輸入界面

圖11　修改聯(lián)系人生成圖

該規(guī)格說(shuō)明自動(dòng)生成器可以成功生成小規(guī)模系統(tǒng)的Z規(guī)格說(shuō)明書,為了今后在大規(guī)模系統(tǒng)中進(jìn)行實(shí)現(xiàn)和推廣,該Z規(guī)格說(shuō)明自動(dòng)生成器還需要做以下改進(jìn):

(1)Z規(guī)格說(shuō)明自動(dòng)生成器最終輸出的為.jpg圖像文件,不支持Z語(yǔ)言規(guī)格說(shuō)明的自動(dòng)檢查、自動(dòng)檢驗(yàn)和驗(yàn)證,而且每個(gè)模式就是一個(gè)單獨(dú)的圖像文件,如果是一個(gè)大型系統(tǒng)的Z規(guī)格說(shuō)明的話,就會(huì)產(chǎn)生大量的單獨(dú)的文件,查看起來(lái)耗費(fèi)時(shí)間.所以,需要改進(jìn)輸出格式為PDF文件,查看方便,而且方便讀取其中的內(nèi)容進(jìn)行形式化自動(dòng)檢查.

(2)在輸入?yún)^(qū)域,變量之間對(duì)應(yīng)關(guān)系的輸入框數(shù)量難以滿足大型系統(tǒng)的需求,下一步應(yīng)該實(shí)現(xiàn)動(dòng)態(tài)地添加.

4　結(jié)語(yǔ)

軟件工程是門實(shí)用性的學(xué)科,一個(gè)國(guó)家各個(gè)方面的發(fā)展離不開軟件工程.基于形式化語(yǔ)言的軟件需求規(guī)格說(shuō)明是軟件工程學(xué)科的大趨勢(shì),與國(guó)外軟件工程形式化水平相比,國(guó)內(nèi)軟件工程形式化實(shí)踐任重而道遠(yuǎn).隨著形式化方法研究的不斷深入,形式化規(guī)格說(shuō)明技術(shù)將會(huì)得到更加廣泛的應(yīng)用.本文主要對(duì)自主研發(fā)的Z規(guī)格說(shuō)明自動(dòng)生成器進(jìn)行了簡(jiǎn)單的介紹,并對(duì)其進(jìn)行了應(yīng)用測(cè)試,通過(guò)驗(yàn)證表明該自動(dòng)生成器可以成功地完成小規(guī)模系統(tǒng)的Z語(yǔ)言描述,希望本項(xiàng)研究能夠?yàn)閆語(yǔ)言的推廣做出貢獻(xiàn).在本項(xiàng)研究的基礎(chǔ)上,還可以在通過(guò)語(yǔ)義分析來(lái)生成規(guī)格說(shuō)明、自動(dòng)生成測(cè)試用例等各方面進(jìn)行進(jìn)一步的研究.

參考文獻(xiàn)

1溫晉杰,趙正旭.OpenGL圖形規(guī)范的Z形式化描述.河北省科學(xué)院學(xué)報(bào),2014,31(2):41–48.

2許慶國(guó),繆淮扣,曹曉夏.Object-Z規(guī)格說(shuō)明測(cè)試用例的自動(dòng)生成器.軟件學(xué)報(bào),2011,22(6):1155–1168.

3趙正旭,溫晉杰,趙衛(wèi)華.Z規(guī)范及其使用方法.北京:科學(xué)出版社,2015.

4羊東昭,繆淮扣.Object-Z編輯器的分析、設(shè)計(jì)和實(shí)現(xiàn)[碩士學(xué)位論文].上海:上海大學(xué),2003.

5趙曉峰,趙正旭.虛擬制造環(huán)境的信息規(guī)范及其Z描述研究[學(xué)位論文].濟(jì)南:山東大學(xué),2010.

6趙曉峰,趙正旭.基于Z的虛擬加工仿真環(huán)境規(guī)范技術(shù)研究.系統(tǒng)仿真學(xué)報(bào),2009,21(22):7143–7146.

7劉賈賈.基于小世界網(wǎng)絡(luò)的數(shù)據(jù)格式轉(zhuǎn)換研究及Z語(yǔ)言描述[學(xué)位論文].石家莊:石家莊鐵道大學(xué),2011.

8吳方君,徐升華.用Z形式化描述程序切片.小型微型計(jì)算機(jī)系統(tǒng),2007,28(8):1444–1447.

9繆淮扣,李剛.軟件工程語(yǔ)言—Z.上海:上?？茖W(xué)技術(shù)文獻(xiàn)出版社,1999.

10劉海洋.LATEX入門.北京:電子工業(yè)出版社,2013.

11李瑩,吳江琴.軟件工程形式化方法與語(yǔ)言.杭州:浙江大學(xué)出版社,2010.

12古天龍,常亮.離散數(shù)學(xué).北京:清華大學(xué)出版社,2012.

13International Organization for Standardization.Information Technology—Z Formal Specification Notation—Syntax,Type System and Semantics.ISO/IEC 13568:2002/Cor.1: 2007,C/SC: ISO/IEC JTC 1/SC 22.2007

14Martin AP.Proposal: Community Z Tools Project (CZT).Computing Laboratory Oxford University.Sept.2001.

15Hall A.2014,Community Z Tools Project (CZT): Tools for Editing,Type checking and Animating Z specifications and Related Notations.SourceForge.

16Jacky J.Z2HTML translator.Department of Radiation Oncology,Box 356043,University of Washington/Seattle,Washington 98195-6043 / USA.2015.

17The Unicode Consortium,2006,The Unicode Standard,Version 5.0 (5th Edition),Addison-Wesley Professional.ISBN 0321480910.

18Spivey JM.The Z Notation: A Reference Manual.Second edition,Prentice Hall International (UK)Ltd.1992.

19International Organization for Standardization.Information Technology—Z Formal Specification Notation—Syntax,Type System and Semantics.ISO/IEC 13568:2002,TC/SC: ISO/IEC JTC 1/SC 22.2002.

Z Specification Automatic Generator

ZHAO Zheng-Xu1,WEN Jin-Jie2
1(Shijiazhuang Tiedao University,Shijiazhuang 050043,China)
2(School of Information Science and Technology,Shijiazhuang Tiedao University,Shijiazhuang 050043,China)

Abstract:The formalized Z language can improve the reliability and robustness of the software via using complex mathematical theories.However,only a few people can understand these theories and compile with Z specification.At present,the main research of Z language focuses on the theoretical research.There is no corresponding tools support the automatic generation of Z specification.The research of Z specification automatic generator introduced in this article can help with the compilation of the Z specification and cut the cost of formal development.This automatic generator has great significance for the large-scale promotion of the Z language.

Key words:Z language; formalization; automatic generator; specification; semantic analysis

收稿時(shí)間:①2015-08-06;收到修改稿時(shí)間:2015-10-19