Ada 2020 (23日目) - Stable_Properties

契約プログラミングの続き。 引き続き理解が怪しい箇所がありましたらご指摘ください。

経緯

前回は検証のためには事後条件が必要ということを再確認しました。

さて前回のスイッチの例はON/OFFだけでしたが、オブジェクトは通常複数の属性(Adaの属性ではなくてオブジェクト指向で一般に言う属性)を持ちます。 ややこしいのでオブジェクト指向の属性は以降プロパティと表記します。

例えば File_Type のようなものを考えます。 標準ライブラリにあるやつを真似た感じで。

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_TypeIs_OpenMode の2つのプロパティを持ち、それぞれ True/FalseInput/Output の状態を持ちます。 ただし ModeIs_OpenTrue のときのみ意味を持ちます。 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_OpenFalse ですので Open の事前条件を満たしています。

  2. Open の事後条件から Is_OpenTrueModeOutput ですので Put の事前条件を満たしています。

  3. 2で呼ばれた Put の事後条件が書かれていませんので File が今どうなっているのかわかりません。 従って Put を連続して呼んでよいのかわかりません。

おっと GetPut の事後条件を書き忘れていました。

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;
  1. Put の呼び出しでは Is_OpenMode が変わらないことが事後条件から確認できましたのでOKです。

4から8も同じようにOKです。

  1. Reset の呼び出し後の Mode がわかりません。 従って Get の事前条件を満たせているかわかりません。

おっと Reset の事後条件でも Mode のことを書く必要があります。

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;
  1. Reset の呼び出し後も Mode は変化しないことが事後条件から確認できました。 その前の段階では ModeInput ですのでOKです。

  2. Get の事後条件から Is_OpenTrue ですので Close の事前条件を満たしています。

これで不備はなくなりました。 やったー。 面倒くさいですね!

オブジェクトが複数のプロパティを持っていますと in out パラメータを持つサブプログラムの事後条件では毎回ほぼ全てのプロパティについて書かないといけなくなります。 面倒くさいですね!

ほぼ全てのプロパティを書き換えるサブプログラムなんて滅多にないわけです。

Ada 2020での改善

Stable_Propertiesアスペクト

というわけで導入されたのが Stable_Properties です。 滅多に変わらないプロパティを宣言できます。

実際にはオブジェクトを引数に取る関数を指定します。

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_OpenMode が滅多に変わらないプロパティだと宣言しました。 これで ResetGetPut からは事後条件を消すことができます。

その代わり Close では Mode が変わるかもしれないことを再宣言する必要があります。 事後条件で明記している Is_Open については再宣言の必要はありません。

Stable_Properties で宣言された各プロパティは、 not を付けて再宣言されておらず事後条件でも明記されていなければ、事後条件に and で続けるように展開されます。

例ですとこんな感じになるでしょうか。

-- 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

Eiffelの場合

この Stable_Properties もEiffelにはない要素です。 しかしEiffelでも事後条件を沢山書く必要があって面倒なことになっている……とは思えません。 実際Eiffelのコードはかなりシンプルに見えます。 どうなっているのでしょうか。

実はEiffelの総本山の処理系EiffelStudio単独では静的検証はできず追加のアドオンを使う必要があるようです。 そのひとつとしてEVEという検証器が存在しています。

EiffelStudioとEVEの関係はGNATとSPARKの関係、またはVisualStudioとCode Contractsの関係等に近いのでしょう。

SPARKがAdaにはない追加のpragmaやアスペクトを追加しまくっているのと同じようにEVEも追加の記述を必要とするようです。 詳しく知りたい方はEVEのドキュメントを読んでいただくことにして私が斜め読みした結果を雑に書きます。

EVEではmodelと呼ばれる仮想のプロパティを宣言できます。 そして各ルーチン(サブプログラム)においてmodify_modelの宣言がなされたプロパティのみが変更できます。 modify_modelを書かなければ手続きは Current (現在のインスタンス、所謂 thisSelf)の全てのプロパティを変更する、関数は何も変更しないと見做されるようです。

modelの宣言はSPARKのpragma Abstract_State と型に付ける Stable_Properties を合わせたようなもの、各ルーチンのmodify_modelの宣言は各サブプログラムに付ける GlobalStable_Properties => not を合わせたようなもの……にイメージとしては近いのではないでしょうか。

スマートですね。