基于Object-Z生成Python代碼的研究

袁鼎 劉振宇

摘要??? 在本文中，我們將提出一種從OZ到Python的映射去驗(yàn)證這些規(guī)范。在這個(gè)映射中，包括前置條件、后置條件和變量都將被驗(yàn)證，這些都是建立在使用lambda函數(shù)（以下簡(jiǎn)稱L函數(shù)）和Python的編輯器上的。本研究發(fā)現(xiàn)Python對(duì)于開發(fā)從OZ映射到Python的函數(shù)庫(kù)來說是一種相對(duì)完美的語(yǔ)言。

【關(guān)鍵詞】Object-Z Python 面向?qū)ο缶幊?契約式設(shè)計(jì)

1 概述及相關(guān)工作

形式化語(yǔ)言0Z是基于面向?qū)ο缶幊痰模鄬?duì)于其他形式化語(yǔ)言，OZ語(yǔ)言有更加重要的特征，具體如下：

（1）強(qiáng)有力的語(yǔ)義和運(yùn)算（謂詞運(yùn)算和集合論）。

（2）強(qiáng)大的對(duì)象支持。

（3）其規(guī)范類型直接和面向?qū)ο缶幊虡?gòu)造相對(duì)應(yīng)。

然而，通過形式化語(yǔ)言來進(jìn)行形式化證明是一項(xiàng)很困難的任務(wù)，它需要許多數(shù)學(xué)技巧，并且要找到一種能夠把0Z語(yǔ)言映射到編程語(yǔ)言，并且在執(zhí)行期間能夠驗(yàn)證這種規(guī)范的方法。許多研究人員已經(jīng)做了許多關(guān)于映射0Z到面向?qū)ο缶幊陶Z(yǔ)言的工作，比如C++和Java等等。這其中有些研究表示的是一種映射方法，它包含了一些0Z結(jié)構(gòu)如基本類型、模式、類、狀態(tài)模式、操作運(yùn)算符、狀態(tài)模式謂詞等等。

此外，有些研究人員還做了關(guān)于映射0Z到包含合并規(guī)范概念的面向?qū)ο笠?guī)范語(yǔ)言方面的研究。這些對(duì)應(yīng)鏈接可以允許系統(tǒng)需求在高級(jí)形式化語(yǔ)言中被明確規(guī)定，并且可以在編程層面進(jìn)行驗(yàn)證。

不同于0Z映射中的C++等編程，Python支持多元模式、動(dòng)態(tài)分類、高級(jí)嵌入式數(shù)據(jù)類型、許多可利用的擴(kuò)展了數(shù)據(jù)計(jì)算能力的擴(kuò)展包。它集合了謂詞運(yùn)算、集合論、定理證明去驗(yàn)證這些文字性的規(guī)范。這使得它非常適合用在科學(xué)化和形式化規(guī)范映射當(dāng)中，本文實(shí)現(xiàn)了映射一部分0Z規(guī)范到Python編程層面的規(guī)范。

2 研究背景

我們先回顧一下0Z的主要結(jié)構(gòu)，我們選擇Python編程去映射0Z的原因，然后考慮通過契約式設(shè)計(jì)去驗(yàn)證從0Z映射到Python的協(xié)議。

2.1 OZ

OZ是Z語(yǔ)言的擴(kuò)充，它在此基礎(chǔ)上增加了面向?qū)ο蟮哪Ｊ綐?gòu)建，比如類和其他面向?qū)ο蟮母拍睿úl(fā)性、單1多繼承等）。Z語(yǔ)言是基于數(shù)學(xué)符號(hào)比如集合論，L函數(shù)和一階謂詞邏輯，Z語(yǔ)言表達(dá)式是使用數(shù)學(xué)函數(shù)和謂詞來進(jìn)行分類的。

在OZ中，類定義由一個(gè)已命名的伴隨可選擇形式化參數(shù)的“盒子”所構(gòu)成。這個(gè)“盒子”介紹一個(gè)基本類型僅僅使用了一個(gè)表達(dá)式或者謂詞，或者可能擁有一個(gè)可見性列表、可繼承的類、本地類型和常量定義。

我們嘗試以一個(gè)OZ規(guī)范為范例，它描述.了一個(gè)簡(jiǎn)易的信用卡銀行賬戶系統(tǒng)。每個(gè)賬戶有兩個(gè)數(shù)據(jù)（當(dāng)前余額和信用額度）和兩個(gè)操作（取出、存入）。該0Z規(guī)范范例將在接下來的章節(jié)中被一步步轉(zhuǎn)化為執(zhí)行代碼。

2.2 Python

Python是一種強(qiáng)大的編程語(yǔ)言，它支持多個(gè)范例、動(dòng)態(tài)分類、自動(dòng)存儲(chǔ)器管理、高層的內(nèi)置數(shù)據(jù)類型、分層的包和許多可供選擇的附加包。這些包擴(kuò)展了它的數(shù)據(jù)計(jì)算、科學(xué)化圖形和圖形化用戶界面編程等方面的能力，這些使它在科學(xué)編程中變得非常有用。

它和OZ語(yǔ)言有許多相似性。他們都是基于面向?qū)ο竽Ｊ剑酥^詞運(yùn)算和集合論。因此，它是一種自然而然更加接近形式化規(guī)范的功能性編程語(yǔ)言。

它有非常簡(jiǎn)單的語(yǔ)法，閱讀它的程序就像是閱讀英文一樣。用它寫的程序僅僅只有用C++等語(yǔ)言編程的代碼量的一半左右。它集中于問題的解決辦法而不是語(yǔ)言本身，因?yàn)樗拈_源特征，如果你避開了所有的系統(tǒng)相關(guān)特征，它的代碼可以被應(yīng)用于許多平臺(tái)而不需要任何改變。

Python和0Z語(yǔ)言有許多相似性。它們都是基于面向?qū)ο竽Ｊ剑酥^詞運(yùn)算和集合論。因此，它是一種自然而然更加接近形式化規(guī)范的功能性編程語(yǔ)言。

2.3 契約式設(shè)計(jì)

契約式設(shè)計(jì)是一.種過去常用來控制兩個(gè)模塊間的交互的軟件驗(yàn)證性方法，它通過基于前置條件和后置條件準(zhǔn)則的精確規(guī)范來確保編程和規(guī)范之間的-致性。對(duì)于Python編程來說，已經(jīng)有許多契約式設(shè)計(jì)包比如PyContract等允許注釋契約表達(dá)式的功能，但是這些包使用了一種不允許擴(kuò)充契約表達(dá)式的語(yǔ)法，它不能表示不變量到類屬性，這些契約也僅僅只能處理本地范圍內(nèi)的函數(shù)變量。

功能契約由前置條件和后置條件組成，在本文中，前置條件修飾符“pre”表示執(zhí)行一個(gè)函數(shù)之前應(yīng)該滿足的條件。同理，后置條件修飾符“post”表示在執(zhí)行完該函數(shù)后必須要達(dá)到的目標(biāo)。這些“pre”和“post”修飾符也可以應(yīng)用于類方法，上。此外，不變量修飾符“inv”表示類實(shí)例無論在調(diào)用前還是調(diào)用后總是返回真。“pre”“post”“inv”修飾符以L函數(shù)作為參數(shù)來驗(yàn)證類或者方法上的約束。

3 OZ到Python的映射

3.1 類定義

OZ中的類模式可以通過封裝本地類型、常量聲明、初始化狀態(tài)模式、零或更多給定狀態(tài)的操作模式來引進(jìn)類的概念。

規(guī)則1：每一個(gè)OZ類模式等同于一個(gè)同名的Python類聲明，不考慮任何形式的通用參數(shù)類型是否退出，因?yàn)镻ython是一種在運(yùn)行時(shí)驗(yàn)證信息類型安全的動(dòng)態(tài)類型檢查語(yǔ)言。

3.2 可見性列表

在OZ可見性列表中，所有發(fā)現(xiàn)的成員對(duì)于類對(duì)象的環(huán)境來說都是可見的。在可見性列表中未被發(fā)現(xiàn)的成員僅對(duì)類的對(duì)象及其所有派生類可見。默認(rèn)情況下，Python中的所有類成

員都是共有的，如果它的名字有兩個(gè)強(qiáng)調(diào)不能被外部類訪問的前綴就表明它是私有的。

規(guī)則2：一個(gè)未在可見性列表中發(fā)現(xiàn)的類的所有成員將通過其名稱預(yù)先用兩個(gè)下劃線預(yù)編譯為私有。這些下劃線將可以通過它的名稱在同一個(gè)類中被訪問，或者通過它的父類名稱在派生類中被訪問，否則默認(rèn)為是公有的。

3.3 常量聲明

在OZ中，常量聲明與類相關(guān)，它有固定值并且不被類的任何操作所改變，但它在有些類中可能有不同。因?yàn)榫帉懞瘮?shù)比編寫類更加容易，而Python對(duì)象可以充當(dāng)函數(shù)對(duì)象，所以我們可以將這些類型聲明映射到由類型條件驗(yàn)證修飾的函數(shù)上。

規(guī)則3：每個(gè)常量聲明都將被映射到一個(gè)由“pre”謂詞修飾的函數(shù)，用來檢驗(yàn)常量類型及其初始化。

3.4 常量模式謂詞

常量模式謂詞是指在模式中為常量提供正確值的謂詞。

規(guī)則4：常量模式謂詞將被映射到使用L函數(shù)來檢查常量正確值的“inv”修飾器。

3.5 狀態(tài)模式

狀態(tài)模式是表示一個(gè)聲明屬性值對(duì)應(yīng)于類變量的構(gòu)造，并通過謂詞來確定它們值之間的正確關(guān)系。

規(guī)則5：在狀態(tài)模式中，每-一個(gè)變量都將被映射到類屬性上，它的狀態(tài)謂詞將被視為一個(gè)不變的類修飾器“inv”。

主變量要么是可見的，要么是不可見的。不可見的變量（屬性）需要從兩個(gè)下劃線符號(hào)開始，因此它不能被外部類修改。如果變量和不變量相關(guān)聯(lián)以確保它的正確性，則該模式必須擁有檢查屬性值的不變量。

3.6 初始狀態(tài)模式

初始狀態(tài)模式?jīng)]有聲明部分，它的謂詞限制了狀態(tài)變量和類常量的可能值。初始模式?jīng)Q定了所有已創(chuàng)建對(duì)象的初始狀態(tài)，并始終命名為init。

規(guī)則6：初始狀態(tài)模式將映射到制定了所有已創(chuàng)建對(duì)象初始值的_init_構(gòu)造函數(shù)。

3.7 操作模式

規(guī)則7：每個(gè)操作模式都將映射到一個(gè)Python方法及其相關(guān)的輸入聲明，其謂詞列表將映射到L前提條件和后置條件的集合。

3.8 對(duì)象交互

我們以兩個(gè)信用卡為類實(shí)例，描述存款，以及不用卡之間的取款及資金轉(zhuǎn)移等基本功能。

3.8.1 輔助變量

輔助變量可能根據(jù)類中出現(xiàn)的主變量而發(fā)生變化，因此主變量的任何更改都會(huì)影響輔助變量，更改主變量的操作必須更新輔助變量。

規(guī)則8：編寫一個(gè)函數(shù)來更新輔助變量，以防主變量值發(fā)生改變，并且用此函數(shù)來修飾類。在調(diào)用類中的任何方法以根據(jù)與這些變量相關(guān)的不變狀態(tài)更改輔助變量之后，將調(diào)用此更新函數(shù)。

在我們的函數(shù)庫(kù)中找到了修飾所有函數(shù)實(shí)現(xiàn)，用于在調(diào)用更改輔助變量的類中的任何方法之后調(diào)用大括號(hào)之間出現(xiàn)的函數(shù)。

3.8.2 初始模式引用

object._init_（self）是對(duì)“object”的初始模式的調(diào)用。

3.8.3 非確定性選擇

非確定性選擇運(yùn)算符用于對(duì)一對(duì)運(yùn)算中的至多一個(gè)運(yùn)算的出現(xiàn)進(jìn)行建模，并且當(dāng)兩個(gè)運(yùn)算都被啟用時(shí)，將非確定性地選擇運(yùn)算。

3.8.4 順序組合

順序組合運(yùn)算符等效于執(zhí)行第一個(gè)運(yùn)算，然后執(zhí)行第二個(gè)運(yùn)算，第一個(gè)運(yùn)算輸出變量被識(shí)別并與具有相同基本名稱的第二個(gè)運(yùn)算的輸入變量等同，這意味順序組合等效于并行組合。映射如下：

OpExp3：=OpExp1;OpExp2

3.8.5 并行組合

并行識(shí)別運(yùn)算符II用作模式管道運(yùn)算符，它通過在一個(gè)操作中識(shí)別和等同輸入變量與具有相同名稱的其它操作中的輸出變量來結(jié)合操作表達(dá)式。并行組合運(yùn)算操作符可以表示如下：

OpExp3：=OpExp1IIOpExp2

規(guī)則9：以上形式的并行運(yùn)算符可以被映射成：

op3=parallel（opl，op2）

where

defparallel（shl，sh2，*kwargs）：

returmlambda*kwargs：sh2（shl（*kwargs））**kwargs是一個(gè)字典，它結(jié)合了兩種模式的輸入，每個(gè)輸入都可以通過字典訪問，例如訪問x的值，我們寫成kwargs[x]。

這對(duì)所有的并行運(yùn)算都有效，如果在第一個(gè)模式的輸出和第二個(gè)模式的輸入中存在具有相同名稱和類型的變量，則第一個(gè)模式調(diào)用參數(shù)傳遞給第二個(gè)模式，該參數(shù)被視為通過引用調(diào)用。

4 總結(jié)與展望

編程語(yǔ)言具有不同的風(fēng)格和范例，具有不同的優(yōu)點(diǎn)和缺點(diǎn)。在將C++和Java編程映射到0Z方面已經(jīng)做了許多的努力，但是流行度和面相對(duì)象編程范例更加傾向于本文中這種映射。Python是一種多范式編程語(yǔ)言，動(dòng)態(tài)類型、高級(jí)內(nèi)置數(shù)據(jù)類型和許多附加軟件包，它包含謂詞演算、數(shù)學(xué)證明、集合論和許多庫(kù)。除此之外，它還可以擴(kuò)展包含新的符號(hào)和特征。

Python和OZ語(yǔ)言有許多相似之處。它們都是基于面向?qū)ο蟮姆妒?集合論和謂詞演算，而且Python是一種函數(shù)式編程語(yǔ)言，它自然更接近形式化規(guī)范。

本工作發(fā)現(xiàn)Python是一種很好的語(yǔ)言，用于開發(fā)庫(kù)來映射0Z規(guī)范，這些規(guī)范使用Python的修飾功能來擴(kuò)展具有前提條件、后置條件和不變式符號(hào)的語(yǔ)言以檢查功能約束。此外，通過編寫這些符號(hào)使其成為可能通過幾個(gè)簡(jiǎn)單的步驟將規(guī)范轉(zhuǎn)換為實(shí)現(xiàn)。實(shí)際上，這些符號(hào)將通過執(zhí)行它們而不是執(zhí)行證明來驗(yàn)證。未來的工作可以完成此處未涉及的所有其它OZ構(gòu)造，并可以將OZ形式規(guī)范轉(zhuǎn)換為自動(dòng)化實(shí)現(xiàn)。

參考文獻(xiàn)

[1]湯小康.基于UML和Z的需求分析到軟件體系結(jié)構(gòu)的映射研究[D].湖南師范大學(xué)，2007.

[2]燕昊.UML建模的形式化研究[D].蘭州大學(xué)，2006.

[3]周瑾，馬應(yīng)龍，李巍等.UML的形式化及其應(yīng)用[J].計(jì)算機(jī)科學(xué)，2005，32（03）：136-140.

[4]文志誠(chéng)，繆淮扣，張新林。基于0bject-Z的形式化驗(yàn)證方法[J].計(jì)算機(jī)科學(xué)，2007，34（05）：247-251.

[5]解方.從UML建模到Z形式化規(guī)范的研究[D].太原理工大學(xué)，2013.

[6]湯小康，王志剛，曹步文.UML用例圖的Z形式規(guī)范[J].計(jì)算機(jī)與現(xiàn)代化，2006（11）：12-13.