Z規格說明自動生成器①

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

?

Z規格說明自動生成器①

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

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

關鍵詞:Z語言; 形式化; 自動生成器; 規約; 語義分析

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

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

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

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

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

1　主要的Z語言編輯工具

一直以來,軟件開發者都期望研發出的軟件具有較高的可行性和魯棒性,形式化方法使用適當的數學分析以提高設計的可靠性和魯棒性.但是,由于采用形式化方法的成本高意味著它們通常只用于開發注重安全性的高度整合的系統.所以,對Z語言輔助工具的研究以降低形式化開發的成本就成為一個研究的熱點.針對Z語言的輔助工具有很多種,但是大多數都不支持于2002年頒布的Z語言ISO標準,關于Z語言的工具在文獻報告中并不多見,主流的Z語言支撐工具可以分為Z獨立系統、Z接口模塊、Z集成插件.Z獨立系統中具有代表性的為“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語言的編輯、類型檢查、文檔結構檢查等工作,輸出的是word文檔,只有自己的計算機上面裝有“Z Word Tools”才可以正確地查看該文檔.“Z Word Tools”具體功能包括:

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

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

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

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

(5)為Z語言規格說明繪制與顯示結構示意圖.

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

圖1　Z Word Tools菜單欄

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

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

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

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

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

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

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

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

2　設計與實現

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

Z規格說明自動生成器的界面有兩個區域,即輸入區域和顯示區域,輸入區域又分為狀態變量的輸入區和變量之間操作關系的輸入區域.如圖2所示.

圖2　Z規格說明自動生成器首頁

在狀態變量的輸入區內可以輸入的內容有以下幾個類型.

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

圖3　模式類型示意圖

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

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

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

圖4　變量種類示意圖

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

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

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

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

顯示區域要根據輸入區域所輸入的信息顯示相應的Z模式框.

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

①Z模式框的顯示

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

②顯示區域的保存

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

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

③特殊符號的顯示

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

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

圖5　顯示原理示意圖

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

表1　特殊符號Unicode編碼表

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

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

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

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

3　實例研究與工具演示

手機是我們日常生活中必不可少的通訊工具,本節選擇聯系人相關操作進行Z語言的描述與驗證.

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

RESPONSE::= Success.

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

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

圖6　初始化模式生成界面

增加聯系人操作會涉及到初始化的變量,所以要涉及初始化模式InitPhone,增加聯系人成功之后,通訊錄中聯系人姓名為PhoneName會改變、通訊錄中聯系人電話PhoneNumber也會變為原有的號碼的集合加上新輸入的聯系人電話,Z模式描述如下:

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

圖7　增加聯系人輸出界面

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

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

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

圖8　刪除聯系人輸入界面

圖9　刪除聯系人生成圖

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

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

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

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

圖10　修改聯系人輸入界面

圖11　修改聯系人生成圖

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

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

(2)在輸入區域,變量之間對應關系的輸入框數量難以滿足大型系統的需求,下一步應該實現動態地添加.

4　結語

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

參考文獻

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

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

3趙正旭,溫晉杰,趙衛華.Z規范及其使用方法.北京:科學出版社,2015.

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

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

6趙曉峰,趙正旭.基于Z的虛擬加工仿真環境規范技術研究.系統仿真學報,2009,21(22):7143–7146.

7劉賈賈.基于小世界網絡的數據格式轉換研究及Z語言描述[學位論文].石家莊:石家莊鐵道大學,2011.

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

9繆淮扣,李剛.軟件工程語言—Z.上海:上海科學技術文獻出版社,1999.

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

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

12古天龍,常亮.離散數學.北京:清華大學出版社,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