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

?

Z規(guī)格說明自動生成器①

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

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

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

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

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

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

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

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

1　主要的Z語言編輯工具

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

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

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

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

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

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

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

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

圖1　Z Word Tools菜單欄

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

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

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

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

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

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

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

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

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

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

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

圖2　Z規(guī)格說明自動生成器首頁

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

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

圖3　模式類型示意圖

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

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

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

圖4　變量種類示意圖

變量名稱: 選擇變量種類之后,我們在可編輯輸入框中輸入相應(yīng)的自定義變量名稱.

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

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

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

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

在Z規(guī)格說明自動生成器具體實施的過程中,主要遇到以下三個問題:

①Z模式框的顯示

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

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

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

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

③特殊符號的顯示

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

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

圖5　顯示原理示意圖

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

表1　特殊符號Unicode編碼表

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

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

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

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

3　實例研究與工具演示

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

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

RESPONSE::= Success.

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

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

圖6　初始化模式生成界面

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4　結(jié)語

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

參考文獻

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

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

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

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

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

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

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

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

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

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

11李瑩,吳江琴.軟件工程形式化方法與語言.杭州:浙江大學(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

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