Boolean Expression

Mikkによって提案されたスキーマ述語コンパイラは、Z仕様をCコードにコンパイルするものである。 Zの基本単位であるZスキーマごとに、関数にパラメータとして渡されたプログラム状態を用いて、スキーマ述語を評価するC関数を生成するアプローチである。 生成されたコードは、スキーマの述語を「ブルートフォース」戦略で評価する。 すなわち、ある状態が与えられると、式をその値に置き換え、真理値表を用いて命題計算式を評価し、データ構造を反復して数量化および集合構文を評価する。 生成されたC関数の複雑さを軽減するために、このアプローチでは、生成されたCコードが常に終了することを保証する最適化ステップを提案する。 コードを最適化するために、本技術はZ言語の「実行可能な」サブセットを定義する。 このサブセットは、命題計算式、有限集合に対する数量化、有限反復に基づく集合構成などの有限述語で構成される。 この技術は、実行可能述語の集合を、ある条件を満たす特殊な非実行可能述語を、 意味を変えずに実行可能述語に変換するルール群によって拡張するものである。 例えば、次の二つの規則は量詞を排除する：

ここでMは集合、変数xはM内の要素、そしてPは述語である。 演算子-は「Z記法スポット」とも呼ばれ、量詞∃と一緒に使うと「そのような」、量詞∀と一緒に使うと「その、」という意味になる。 例えば、∃ x : M – Pは、述語Pが真となるような値xが少なくともMに存在することを意味する。 また、NotOccur(x, P)という条件は、xが述語Pの自由変数でないことを示す。 集合Mは無限であっても、上記の規則を適用して量 子を除去できる限り、コンパイラはM上の量子を用いて仕様をコンパイルすることができる。 公理的あるいは一般的な定義によって導入されるユーザ定義関数については、コンパイラはユーザが対応するコードを提供することを要求する。 Mikkはまた、部分的に定義された仕様の問題に対する解決策を提案している。 彼は、中間形式としてVDM-SLを用い、SchmidtとHörcherが開発したVDM-SLコンパイラを用いて、Z仕様をCコードに変換している。 部分的に定義された式、すなわち、定義領域外で評価されたときに未定義 (⊥と表記) と評価される可能性がある関数または関係を扱う場合、このアプローチは例外ハンドラーを生成します。 McDonaldらは、コンテナクラスのOjbect-Z仕様を、最適化、構造マッピング、述語変換の3段階でC++コードに変換している。 最適化では、定数変数をその値に置き換え、二次変数やスキーマ・エンリッチメントを削除するなど、いくつかの段階を経て、その後の翻訳を簡略化するために仕様を整理している。 構造マッピングでは、Object-Z仕様の構造を、対応するコード要素にマッピングする。 定数や変数は適切な初期化を施した変数に、変数の型は原始的なC++の型や技術で使用するZ toolkitライブラリの対応するクラスに、それぞれマッピングします。 たとえば、整数とブーリアン型を int に、整数セットの型を z_set<int > にマップしています。 初期化スキーマをコンストラクタに、操作スキーマをメンバ関数に対応付け、クラス不変性をチェックするための特別なメンバ関数 inv() を作成し、例外スキーマごとに例外クラスを生成します。

述語 DeepL 変換では、述語の評価ではなく、プログラムの状態をチェックするコードを生成する方法に焦点を当てます。 例えば、inv()関数が他のメンバ関数を呼び出さないように翻訳し、無限再帰を回避している。

Richardsonらは、タイムクリティカルシステムに注目し、Zと時間間隔論理の組み合わせを扱い、記号的解釈によるテストオークルに仕様の変換を提案している。 記号的解釈は、データと制御のマッピングを参照し、刺激入力と初期状態変数に仕様の記号名を割り当てる。 そして、仕様書の各制御経路を解釈し、すなわち各仕様制御点における記号の状態から仕様データ上の条件を表すアサーションを作成する。 仕様制御点とは、パラメータ化されたイベント、遷移、操作などの関連要素である。 Z仕様の記号的解釈の後、オラクル情報は関連するZスキーマとそれに対応するアサーションのリストとして表現され、スキーマが呼び出された場合にチェックが行われる。 テストケースの実行は、具体的なテスト入力を参照し、そこから具体的な変数とイベントがテストクラス内の対応するものに束縛される（各テストクラスはテスト入力のパーティションである）。 テストケースの実行は実行プロファイルを生成し、実行プロファイルに含まれる具体的なイベントと変数の値は、オラクル情報との整合性をチェックするためにオラクル レベルにマッピングされる。

アサーション言語は仕様をソースコードにマージするので、翻訳の問題は単純化されるが解消はされない。 アサーションは、さまざまな言語や方法論によってサポートされています。 Design by contractは、コードとアサーションの共同設計を仮定したソフトウェア設計パラダイムである。 コントラクトによる設計はMeyerによって提案され、プログラミング言語Eiffelで完全にサポートされている。 Zのような一般的な仕様言語とは異なり、Eiffelではコントラクトと呼ばれる仕様がソースコードにマージされ、適切に設計されたインターフェースを介して通信するソフトウェアコンポーネントの義務や利益を定義している。 コントラクトをサポートする言語では、クライアントの義務や利益は、サービス提供者の事前条件や事後条件として表現される。

コントラクトは多くの言語に拡張されていますが、iContract は Java でコントラクトをサポートする最初のツールです。 iContract では、契約は特別なタグを使用したコードコメントとして記述されます。 iContract がサポートする契約は、普遍量化 (∀)、存在量化 (∃)、含意 (→) などのいくつかの構文拡張を除いて、Java 構文に準拠したブール式です。 これらの拡張は、Javaコードへの翻訳を簡単にするために設計されています。 例えば the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: “if C then check I.”