基于C++STL技術(shù)實現(xiàn)Z模式自動求精的研究

文 欣

（廈門工學(xué)院計算機(jī)科學(xué)與工程系，廈門 361021）

1 引言

Z是一種形式化規(guī)格說明語言，具有嚴(yán)謹(jǐn)、準(zhǔn)確的特點，主要應(yīng)用航空航天、軍事等無法重復(fù)測試的關(guān)鍵系統(tǒng)領(lǐng)域。但是Z不是一種可執(zhí)行級語言，因此提出了Z語言向高級語言（C++）自動求精，從而實現(xiàn)從需求說明到編碼的自動化。

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

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

2 Z到C++的數(shù)據(jù)求精和過程求精

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

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

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

集合操作轉(zhuǎn)C++代碼

3 Z模式求精實例

以教師工資系統(tǒng)為例，增加教師工資模式為AddSalary，該模式中會涉及到初始模式，使用符號“Δ”表示模式的包含，系統(tǒng)中教師工資變?yōu)樵瓉淼募霞尤胄略黾拥哪Ｊ剑撃Ｊ矫枋鋈缦拢?/p>

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

應(yīng)用C++STL技術(shù)將上述模式轉(zhuǎn)成C++語言，不管是增加教師工資還是刪除教師工資，首先都要判斷該教師是否在系統(tǒng)中，函數(shù)模板如下：

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

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

4 結(jié)束語

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