基于C++STL技術實現Z模式自動求精的研究

文 欣

（廈門工學院計算機科學與工程系，廈門 361021）

1 引言

Z是一種形式化規格說明語言，具有嚴謹、準確的特點，主要應用航空航天、軍事等無法重復測試的關鍵系統領域。但是Z不是一種可執行級語言，因此提出了Z語言向高級語言（C++）自動求精，從而實現從需求說明到編碼的自動化。

模式是組成Z語言的基本單位，它分為說明部分和謂詞部分，說明部分定義一些狀態或模式變量，謂詞部分一般是謂詞公式。以教師工資系統為例，假設教師姓名定義為TSName，教師工資定義為TSSalary。定義教師名和工資的類型分別為Name和Salary，操作后系統給出的提示信息是：Report：=ok|already exit。初始化模式為InitSalary，形式如下：

模式中的name、salary后跟著一個“?”代表輸入變量，Report后跟一個”!”代表輸出變量。P Name、P Salary是Z的冪集類型，初始時系統沒有任何教師及工資記錄，因此謂詞部分定義為空。

2 Z到C++的數據求精和過程求精

C++STL模板提供了大量數據結構的算法，不僅支持對容器的操作，還支持用戶自己定義的數據類型。Z到C++的求精主要包括數據類型求精和過程求精。

Z的整數類型直接轉成C++中的int或long類型，如n1，n2，…，nmZ，轉成C++表示為：int n1，n2，… nm.。Z中給定集合可用通用模板結構對類型進行求精，如變量elem：Book，轉成C++的代碼如下：template＜Book＞Book elem。Z的冪集類型可用C++中的set容器來轉換，如上模式的TSName：P Name轉C++代碼為：set＜Name＞TSName。關系類型如R A←→B在C++中的可表示為：set＜pair＜A，B＞＞R。序列類型用vector容器表示，如Z的序列X seq TypeName可轉為：vector＜TypeName＞X。Z的包類型如X bag TypeName可表示為map＜TypeName，count＞，其中count表示每個元素在出現的次數。

Z的過程求精主要是對集合類型的一些常用操作，如集合中增加元素，刪除元素、判斷元素是否在集合中，集合的交集、并集、補集，集合的子集操作等。下表主要給出集合中一些基本操作求精結果：

集合操作轉C++代碼

3 Z模式求精實例

以教師工資系統為例，增加教師工資模式為AddSalary，該模式中會涉及到初始模式，使用符號“Δ”表示模式的包含，系統中教師工資變為原來的集合加入新增加的模式，該模式描述如下：

刪除教師工資模式為DeleteSalary，當要刪除的教師名字時工資也應一起刪除，此模式涉及到增加教師工資模式，該模式描述如下：

應用C++STL技術將上述模式轉成C++語言，不管是增加教師工資還是刪除教師工資，首先都要判斷該教師是否在系統中，函數模板如下：

isMember（）方法是判斷教師是否在教師工資系統中，使用fi nd方法從頭到尾進行查找，如果找到該教師已經在系統中返回真，否則返回假。

addSalary方法功能是插入教師工資，使用insert（）方法進行插入

4 結束語

Z說明向C++語言的自動求精是一個極其復雜的過程，想要Z應用在整個軟件開發周期還存在許多問題，如怎樣建立一個合理正確的Z模式對大多數開發人員還存在一定難度，Z的過程求精還有一些問題需要改進。如果Z向C++能夠完全自動化將對未來的軟件開發有著重大意義。