Ada 202x (22日目) - Default_Initial_Condition ============================================= .. post:: Dec 22, 2019 :tags: ada, ada_2022 検証の流れに戻って今回から契約プログラミングです。 引き続き理解が怪しい箇所がありましたらご指摘ください。 経緯 ---- 「契約による設計」ではなく契約プログラミングです。 (「Design by Contract」は米Eiffel Softwareの商標です。 「契約プログラミング」は商標を回避するためD言語等で使用されています。) ……というのはさておき。 Meyer先生の「オブジェクト指向入門」やEiffelのドキュメントにも書いてますように事前条件/事後条件というのは直前の事後条件が直後の事前条件を満たすように組み立てる必要があります。 契約の検証は、各変数について直前の事後条件や不変条件、if文等で満たされた条件が直後の事前条件を内含(implies)しているかどうかをチェックするということです。 そのため言語や処理系等の事情によってはEiffelにない要素も必要になります。 Ada 202xではアクセスの競合チェックのための ``Global`` アスペクトも元はSPARKが導入したものです。 他のAda特有の事情としてデフォルト初期化があります。 Eiffelではデフォルト値は ``0`` や ``Null`` 等と決まっていますしそれで足りなければ生成プロシージャ(所謂コンストラクタ)を呼ぶ必要がありますので生成プロシージャの事後条件でインスタンスの状態を表明できます。 Adaではデフォルト初期化をカスタマイズできますし抽象型にすれば内容を隠すこともできます。 .. code-block:: 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スイッチを考えましても抽象型にしてしまいますとデフォルト初期化がどちらになるかわかりませんので検証できなくなります。 .. code-block:: ada 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; .. code-block:: ada 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`` アスペクトでデフォルト初期化の事後条件を書けるようになりました。 .. code-block:: ada 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** .. _`AI12-0265-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0265-1.txt .. _`AI12-0332-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0332-1.txt