Ada 202x (22日目) - Default_Initial_Condition¶
検証の流れに戻って今回から契約プログラミングです。 引き続き理解が怪しい箇所がありましたらご指摘ください。
経緯¶
「契約による設計」ではなく契約プログラミングです。 (「Design by Contract」は米Eiffel Softwareの商標です。 「契約プログラミング」は商標を回避するためD言語等で使用されています。)
……というのはさておき。
Meyer先生の「オブジェクト指向入門」やEiffelのドキュメントにも書いてますように事前条件/事後条件というのは直前の事後条件が直後の事前条件を満たすように組み立てる必要があります。
契約の検証は、各変数について直前の事後条件や不変条件、if文等で満たされた条件が直後の事前条件を内含(implies)しているかどうかをチェックするということです。
そのため言語や処理系等の事情によってはEiffelにない要素も必要になります。
Ada 202xではアクセスの競合チェックのための Global アスペクトも元はSPARKが導入したものです。
他のAda特有の事情としてデフォルト初期化があります。
Eiffelではデフォルト値は 0 や Null 等と決まっていますしそれで足りなければ生成プロシージャ(所謂コンストラクタ)を呼ぶ必要がありますので生成プロシージャの事後条件でインスタンスの状態を表明できます。
Adaではデフォルト初期化をカスタマイズできますし抽象型にすれば内容を隠すこともできます。
package Pkg1 is
type U is private;
type A is private;
type C is private;
type R is private;
private
type U is range 0 .. Integer'Last
with Default_Value => 1;
type A is array (1 .. 2) of Integer
with Default_Component_Value => 2;
type C is new Ada.Finalization.Controlled with null record;
overriding procedure Initialize (Object : in out C); -- 副作用も起こせる
type R is record
Element : Integer := Get_Value (0); -- 関数呼び出しも可能
Controlled_Part : C; -- 上のInitializeが呼ばれる
end record;
end Pkg1;
このようにパッケージの公開部だけでは何が起きるのか全くわかりません。
例えば2つの状態を取る単純なON/OFFスイッチを考えましても抽象型にしてしまいますとデフォルト初期化がどちらになるかわかりませんので検証できなくなります。
package Pkg2 is
type Switch is private;
function Is_On (Object : Switch) return Boolean;
function Is_Off (Object : Switch) return Boolean is (not Is_On (Object));
procedure On (Object : in out Switch)
with
Pre => Is_Off (Object),
Post => Is_On (Object);
procedure Off (Object : in out Switch);
with
Pre => Is_On (Object),
Post => Is_Off (Object);
private
-- 省略
end Pkg2;
with Pkg_2;
procedure Main is
X : Pkg_2.Switch;
begin
Pkg_2.On (X); -- Pre => Is_Off (X) を満たしているのか不明
Pkg_2.Off (X);
end Main;
デフォルト初期化にも事後条件が必要です。
Ada 202xでの改善¶
Default_Initial_Conditionアスペクト¶
Default_Initial_Condition アスペクトでデフォルト初期化の事後条件を書けるようになりました。
package Pkg2 is
type Switch is private;
with Default_Initial_Condition => Is_Off (Switch);
function Is_On (Object : Switch) return Boolean;
function Is_Off (Object : Switch) return Boolean is (not Is_On (Object));
procedure On (Object : in out Switch)
with
Pre => Is_Off (Object),
Post => Is_On (Object);
procedure Off (Object : in out Switch);
with
Pre => Is_On (Object),
Post => Is_Off (Object);
private
-- 省略
end Pkg2;
デフォルト初期化後はOFFとわかりましたので上の例で最初に On を呼んでいるのは妥当と判断できます。
やはりこれもSPARKからの逆輸入となります。
念の為に繰り返しますがAdaの事前条件/事後条件は実行時のチェックです。
Default_Initial_Condition もデフォルト初期化に対するpragma Assert 相当機能程度の意味しかありません。
静的にチェックしたいのであればSPARKを使う必要があります。
関連AI¶
AI12-0265-1 Default_Initial_Condition for types
AI12-0332-1 Implementation Permission for Default_Initial_Condition