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

袁鼎 劉振宇

摘要??? 在本文中，我們將提出一種從OZ到Python的映射去驗證這些規范。在這個映射中，包括前置條件、后置條件和變量都將被驗證，這些都是建立在使用lambda函數（以下簡稱L函數）和Python的編輯器上的。本研究發現Python對于開發從OZ映射到Python的函數庫來說是一種相對完美的語言。

【關鍵詞】Object-Z Python 面向對象編程 契約式設計

1 概述及相關工作

形式化語言0Z是基于面向對象編程的，相對于其他形式化語言，OZ語言有更加重要的特征，具體如下：

（1）強有力的語義和運算（謂詞運算和集合論）。

（2）強大的對象支持。

（3）其規范類型直接和面向對象編程構造相對應。

然而，通過形式化語言來進行形式化證明是一項很困難的任務，它需要許多數學技巧，并且要找到一種能夠把0Z語言映射到編程語言，并且在執行期間能夠驗證這種規范的方法。許多研究人員已經做了許多關于映射0Z到面向對象編程語言的工作，比如C++和Java等等。這其中有些研究表示的是一種映射方法，它包含了一些0Z結構如基本類型、模式、類、狀態模式、操作運算符、狀態模式謂詞等等。

此外，有些研究人員還做了關于映射0Z到包含合并規范概念的面向對象規范語言方面的研究。這些對應鏈接可以允許系統需求在高級形式化語言中被明確規定，并且可以在編程層面進行驗證。

不同于0Z映射中的C++等編程，Python支持多元模式、動態分類、高級嵌入式數據類型、許多可利用的擴展了數據計算能力的擴展包。它集合了謂詞運算、集合論、定理證明去驗證這些文字性的規范。這使得它非常適合用在科學化和形式化規范映射當中，本文實現了映射一部分0Z規范到Python編程層面的規范。

2 研究背景

我們先回顧一下0Z的主要結構，我們選擇Python編程去映射0Z的原因，然后考慮通過契約式設計去驗證從0Z映射到Python的協議。

2.1 OZ

OZ是Z語言的擴充，它在此基礎上增加了面向對象的模式構建，比如類和其他面向對象的概念（并發性、單1多繼承等）。Z語言是基于數學符號比如集合論，L函數和一階謂詞邏輯，Z語言表達式是使用數學函數和謂詞來進行分類的。

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

我們嘗試以一個OZ規范為范例，它描述.了一個簡易的信用卡銀行賬戶系統。每個賬戶有兩個數據（當前余額和信用額度）和兩個操作（取出、存入）。該0Z規范范例將在接下來的章節中被一步步轉化為執行代碼。

2.2 Python

Python是一種強大的編程語言，它支持多個范例、動態分類、自動存儲器管理、高層的內置數據類型、分層的包和許多可供選擇的附加包。這些包擴展了它的數據計算、科學化圖形和圖形化用戶界面編程等方面的能力，這些使它在科學編程中變得非常有用。

它和OZ語言有許多相似性。他們都是基于面向對象模式，包含了謂詞運算和集合論。因此，它是一種自然而然更加接近形式化規范的功能性編程語言。

它有非常簡單的語法，閱讀它的程序就像是閱讀英文一樣。用它寫的程序僅僅只有用C++等語言編程的代碼量的一半左右。它集中于問題的解決辦法而不是語言本身，因為它的開源特征，如果你避開了所有的系統相關特征，它的代碼可以被應用于許多平臺而不需要任何改變。

Python和0Z語言有許多相似性。它們都是基于面向對象模式，包含了謂詞運算和集合論。因此，它是一種自然而然更加接近形式化規范的功能性編程語言。

2.3 契約式設計

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

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

3 OZ到Python的映射

3.1 類定義

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

規則1：每一個OZ類模式等同于一個同名的Python類聲明，不考慮任何形式的通用參數類型是否退出，因為Python是一種在運行時驗證信息類型安全的動態類型檢查語言。

3.2 可見性列表

在OZ可見性列表中，所有發現的成員對于類對象的環境來說都是可見的。在可見性列表中未被發現的成員僅對類的對象及其所有派生類可見。默認情況下，Python中的所有類成

員都是共有的，如果它的名字有兩個強調不能被外部類訪問的前綴就表明它是私有的。

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

3.3 常量聲明

在OZ中，常量聲明與類相關，它有固定值并且不被類的任何操作所改變，但它在有些類中可能有不同。因為編寫函數比編寫類更加容易，而Python對象可以充當函數對象，所以我們可以將這些類型聲明映射到由類型條件驗證修飾的函數上。

規則3：每個常量聲明都將被映射到一個由“pre”謂詞修飾的函數，用來檢驗常量類型及其初始化。

3.4 常量模式謂詞

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

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

3.5 狀態模式

狀態模式是表示一個聲明屬性值對應于類變量的構造，并通過謂詞來確定它們值之間的正確關系。

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

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

3.6 初始狀態模式

初始狀態模式沒有聲明部分，它的謂詞限制了狀態變量和類常量的可能值。初始模式決定了所有已創建對象的初始狀態，并始終命名為init。

規則6：初始狀態模式將映射到制定了所有已創建對象初始值的_init_構造函數。

3.7 操作模式

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

3.8 對象交互

我們以兩個信用卡為類實例，描述存款，以及不用卡之間的取款及資金轉移等基本功能。

3.8.1 輔助變量

輔助變量可能根據類中出現的主變量而發生變化，因此主變量的任何更改都會影響輔助變量，更改主變量的操作必須更新輔助變量。

規則8：編寫一個函數來更新輔助變量，以防主變量值發生改變，并且用此函數來修飾類。在調用類中的任何方法以根據與這些變量相關的不變狀態更改輔助變量之后，將調用此更新函數。

在我們的函數庫中找到了修飾所有函數實現，用于在調用更改輔助變量的類中的任何方法之后調用大括號之間出現的函數。

3.8.2 初始模式引用

object._init_（self）是對“object”的初始模式的調用。

3.8.3 非確定性選擇

非確定性選擇運算符用于對一對運算中的至多一個運算的出現進行建模，并且當兩個運算都被啟用時，將非確定性地選擇運算。

3.8.4 順序組合

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

OpExp3：=OpExp1;OpExp2

3.8.5 并行組合

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

OpExp3：=OpExp1IIOpExp2

規則9：以上形式的并行運算符可以被映射成：

op3=parallel（opl，op2）

where

defparallel（shl，sh2，*kwargs）：

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

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

4 總結與展望

編程語言具有不同的風格和范例，具有不同的優點和缺點。在將C++和Java編程映射到0Z方面已經做了許多的努力，但是流行度和面相對象編程范例更加傾向于本文中這種映射。Python是一種多范式編程語言，動態類型、高級內置數據類型和許多附加軟件包，它包含謂詞演算、數學證明、集合論和許多庫。除此之外，它還可以擴展包含新的符號和特征。

Python和OZ語言有許多相似之處。它們都是基于面向對象的范式.集合論和謂詞演算，而且Python是一種函數式編程語言，它自然更接近形式化規范。

本工作發現Python是一種很好的語言，用于開發庫來映射0Z規范，這些規范使用Python的修飾功能來擴展具有前提條件、后置條件和不變式符號的語言以檢查功能約束。此外，通過編寫這些符號使其成為可能通過幾個簡單的步驟將規范轉換為實現。實際上，這些符號將通過執行它們而不是執行證明來驗證。未來的工作可以完成此處未涉及的所有其它OZ構造，并可以將OZ形式規范轉換為自動化實現。

參考文獻

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

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

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

[4]文志誠，繆淮扣，張新林。基于0bject-Z的形式化驗證方法[J].計算機科學，2007，34（05）：247-251.

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

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