Ada 202x (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_Type は Is_Open と Mode の2つのプロパティを持ち、それぞれ True/False と Input/Output の状態を持ちます。
ただし Mode は Is_Open が True のときのみ意味を持ちます。
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;
この使用例を手動検証してみましょう。
Default_Initial_Conditionから最初はIs_OpenはFalseですのでOpenの事前条件を満たしています。Openの事後条件からIs_OpenはTrue、ModeはOutputですのでPutの事前条件を満たしています。2で呼ばれた
Putの事後条件が書かれていませんのでFileが今どうなっているのかわかりません。 従ってPutを連続して呼んでよいのかわかりません。
おっと Get と Put の事後条件を書き忘れていました。
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;
Putの呼び出しではIs_OpenとModeが変わらないことが事後条件から確認できましたのでOKです。
4から8も同じようにOKです。
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;
Resetの呼び出し後もModeは変化しないことが事後条件から確認できました。 その前の段階ではModeはInputですのでOKです。Getの事後条件からIs_OpenはTrueですのでCloseの事前条件を満たしています。
これで不備はなくなりました。 やったー。 面倒くさいですね！
オブジェクトが複数のプロパティを持っていますと in out パラメータを持つサブプログラムの事後条件では毎回ほぼ全てのプロパティについて書かないといけなくなります。
面倒くさいですね！
ほぼ全てのプロパティを書き換えるサブプログラムなんて滅多にないわけです。
Ada 202xでの改善¶
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_Open と Mode が滅多に変わらないプロパティだと宣言しました。
これで Reset 、 Get 、 Put からは事後条件を消すことができます。
その代わり 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¶
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という検証器が存在しています。
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 を合わせたようなもの……にイメージとしては近いのではないでしょうか。
スマートですね。