Ada 202x (23日目) - Stable_Properties ===================================== .. post:: Dec 23, 2019 :tags: ada, ada_2022 契約プログラミングの続き。 引き続き理解が怪しい箇所がありましたらご指摘ください。 経緯 ---- 前回は検証のためには事後条件が必要ということを再確認しました。 さて前回のスイッチの例はON/OFFだけでしたが、オブジェクトは通常複数の属性(Adaの属性ではなくてオブジェクト指向で一般に言う属性)を持ちます。 ややこしいのでオブジェクト指向の属性は以降プロパティと表記します。 例えば ``File_Type`` のようなものを考えます。 標準ライブラリにあるやつを真似た感じで。 .. code-block:: ada package My_IO is type File_Type is limited private with Default_Initial_Condition => not Is_Open (File_Type); type Mode_Type is (Input, Output); function Is_Open (X : File_Type) return Boolean; function Mode (X : File_Type) return Mode_Type; procedure Open (X : in out File_Type; Mode : in Mode_Type) with Pre => not Is_Open (X), Post => Is_Open (X) and then My_IO.Mode (X) = Mode; procedure Close (X : in out File_Type) with Pre => Is_Open (X), Post => not Is_Open (X); procedure Reset (X : in out File_Type) with Pre => Is_Open (X), Post => Is_Open (X); procedure Get (X : in out File_Type; Item : out Character) with Pre => Is_Open (X) and then Mode (X) = Input; procedure Put (X : in out File_Type; Item : in Character) with Pre => Is_Open (X) and then Mode (X) = Output; private -- 省略 end My_IO; この ``File_Type`` は ``Is_Open`` と ``Mode`` の2つのプロパティを持ち、それぞれ ``True``/``False`` と ``Input``/``Output`` の状態を持ちます。 ただし ``Mode`` は ``Is_Open`` が ``True`` のときのみ意味を持ちます。 Adaには言語仕様としてのプロパティはありませんので関数で表現しています。 使用例も適当に用意します。 .. code-block:: ada with My_IO; procedure Main is File : My_IO.File_Type; Item : Character; begin My_IO.Open (File, My_IO.Output); -- 1 My_IO.Put (File, 'A'); -- 2 My_IO.Put (File, 'B'); -- 3 My_IO.Close (File); -- 4 My_IO.Open (File, My_IO.Input); -- 5 My_IO.Get (File, Item); -- 6 My_IO.Get (File, Item); -- 7 My_IO.Reset (File); -- 8 My_IO.Get (File, Item); -- 9 My_IO.Close (File); -- 10 end Main; この使用例を手動検証してみましょう。 1. ``Default_Initial_Condition`` から最初は ``Is_Open`` は ``False`` ですので ``Open`` の事前条件を満たしています。 2. ``Open`` の事後条件から ``Is_Open`` は ``True`` 、 ``Mode`` は ``Output`` ですので ``Put`` の事前条件を満たしています。 3. 2で呼ばれた ``Put`` の事後条件が書かれていませんので ``File`` が今どうなっているのかわかりません。 従って ``Put`` を連続して呼んでよいのかわかりません。 おっと ``Get`` と ``Put`` の事後条件を書き忘れていました。 .. code-block:: ada package My_IO is -- 省略 procedure Get (X : in out File_Type; Item : out Character) with Pre => Is_Open (X) and then Mode (X) = Input, Post => Is_Open (X) and then Mode (X) = Input; procedure Put (X : in out File_Type; Item : in Character) with Pre => Is_Open (X) and then Mode (X) = Output, Post => Is_Open (X) and then Mode (X) = Output; -- 省略 end My_IO; 3. ``Put`` の呼び出しでは ``Is_Open`` と ``Mode`` が変わらないことが事後条件から確認できましたのでOKです。 4から8も同じようにOKです。 9. ``Reset`` の呼び出し後の ``Mode`` がわかりません。 従って ``Get`` の事前条件を満たせているかわかりません。 おっと ``Reset`` の事後条件でも ``Mode`` のことを書く必要があります。 .. code-block:: ada package My_IO is -- 省略 procedure Reset (X : in out File_Type) with Pre => Is_Open (X), Post => Is_Open (X) and Mode (X) = Mode (X)'Old; -- 省略 end My_IO; 9. ``Reset`` の呼び出し後も ``Mode`` は変化しないことが事後条件から確認できました。 その前の段階では ``Mode`` は ``Input`` ですのでOKです。 10. ``Get`` の事後条件から ``Is_Open`` は ``True`` ですので ``Close`` の事前条件を満たしています。 これで不備はなくなりました。 やったー。 面倒くさいですね！ オブジェクトが複数のプロパティを持っていますと ``in out`` パラメータを持つサブプログラムの事後条件では毎回ほぼ全てのプロパティについて書かないといけなくなります。 面倒くさいですね！ ほぼ全てのプロパティを書き換えるサブプログラムなんて滅多にないわけです。 Ada 202xでの改善 ---------------- Stable_Propertiesアスペクト +++++++++++++++++++++++++++ というわけで導入されたのが ``Stable_Properties`` です。 滅多に変わらないプロパティを宣言できます。 実際にはオブジェクトを引数に取る関数を指定します。 .. code-block:: ada package My_IO is type File_Type is limited private with Default_Initial_Condition => not Is_Open (File_Type), Stable_Properties => (Is_Open, Mode); type Mode_Type is (Input, Output); function Is_Open (X : File_Type) return Boolean; function Mode (X : File_Type) return Mode_Type; procedure Open (X : in out File_Type; Mode : in Mode_Type) with Pre => not Is_Open (X), Post => Is_Open (X) and then My_IO.Mode (X) = Mode; procedure Close (X : in out File_Type) with Stable_Properties => not Mode, Pre => Is_Open (X), Post => not Is_Open (X); procedure Reset (X : in out File_Type) with Pre => Is_Open (X); procedure Get (X : in out File_Type; Item : out Character) with Pre => Is_Open (X) and then Mode (X) = Input; procedure Put (X : in out File_Type; Item : in Character) with Pre => Is_Open (X) and then Mode (X) = Output; private -- 省略 end My_IO; ``File_Type`` の型宣言で ``Is_Open`` と ``Mode`` が滅多に変わらないプロパティだと宣言しました。 これで ``Reset`` 、 ``Get`` 、 ``Put`` からは事後条件を消すことができます。 その代わり ``Close`` では ``Mode`` が変わるかもしれないことを再宣言する必要があります。 事後条件で明記している ``Is_Open`` については再宣言の必要はありません。 ``Stable_Properties`` で宣言された各プロパティは、 ``not`` を付けて再宣言されておらず事後条件でも明記されていなければ、事後条件に ``and`` で続けるように展開されます。 例ですとこんな感じになるでしょうか。 .. code-block:: ada -- This is an image! package My_IO is -- 省略 procedure Open (X : in out File_Type; Mode : in Mode_Type) with Pre => not Is_Open (X), Post => Is_Open (X) and then My_IO.Mode (X) = Mode; -- 明記しているためそのまま procedure Close (X : in out File_Type) with Stable_Properties => not Mode, Pre => Is_Open (X), Post => not Is_Open (X); -- Is_Openは明記しておりModeはnot Modeのためそのまま procedure Reset (X : in out File_Type) with Pre => Is_Open (X), Post => Is_Open (X) = Is_Open (X)'Old and Mode (X) = Mode (X)'Old; -- 自動生成 procedure Get (X : in out File_Type; Item : out Character) with Pre => Is_Open (X) and then Mode (X) = Input, Post => Is_Open (X) = Is_Open (X)'Old and Mode (X) = Mode (X)'Old; -- 自動生成 procedure Put (X : in out File_Type; Item : in Character) with Pre => Is_Open (X) and then Mode (X) = Output, Post => Is_Open (X) = Is_Open (X)'Old and Mode (X) = Mode (X)'Old; -- 自動生成 end My_IO; この ``Stable_Properties`` はRandy先生の発案らしく(珍しく)SPARKからの逆輸入ではありません。 そのため現バージョンのSPARKでこの例を試すことはできません。 関連AI ------ - `AI12-0187-1`_ **Stable properties of abstract data types** - `AI12-0285-1`_ **Syntax for Stable_Properties aspects** Eiffelの場合 ------------ この ``Stable_Properties`` もEiffelにはない要素です。 しかしEiffelでも事後条件を沢山書く必要があって面倒なことになっている……とは思えません。 実際Eiffelのコードはかなりシンプルに見えます。 どうなっているのでしょうか。 実はEiffelの総本山の処理系EiffelStudio単独では静的検証はできず追加のアドオンを使う必要があるようです。 そのひとつとしてEVEという検証器が存在しています。 | http://se.inf.ethz.ch/research/eve/ EiffelStudioとEVEの関係はGNATとSPARKの関係、またはVisualStudioとCode Contractsの関係等に近いのでしょう。 SPARKがAdaにはない追加のpragmaやアスペクトを追加しまくっているのと同じようにEVEも追加の記述を必要とするようです。 詳しく知りたい方はEVEのドキュメントを読んでいただくことにして私が斜め読みした結果を雑に書きます。 EVEではmodelと呼ばれる仮想のプロパティを宣言できます。 そして各ルーチン(サブプログラム)においてmodify_modelの宣言がなされたプロパティのみが変更できます。 modify_modelを書かなければ手続きは ``Current`` (現在のインスタンス、所謂 ``this`` や ``Self``)の全てのプロパティを変更する、関数は何も変更しないと見做されるようです。 modelの宣言はSPARKのpragma ``Abstract_State`` と型に付ける ``Stable_Properties`` を合わせたようなもの、各ルーチンのmodify_modelの宣言は各サブプログラムに付ける ``Global`` と ``Stable_Properties => not`` を合わせたようなもの……にイメージとしては近いのではないでしょうか。 スマートですね。 .. _`AI12-0187-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0187-1.txt .. _`AI12-0285-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0285-1.txt