Ada 202x (26日目) - 契約と継承 ============================== .. post:: Dec 26, 2019 :tags: ada, ada_2022 一番理解も説明も難しいところが来てしまいました……。 怪しい箇所がありましたらご指摘ください。 遠慮なく。 ええもう本当に。 リスコフの置換原則 ------------------ 継承で大事なことはリスコフの置換原則(Liskov substitution principle、LSP)を守ることです。 基底型の性質は全て派生型で満たされなければならない(置換可能性)というやつです。 しかし実際にこれを守るのは非常に難しいです。 理解するのも問題のないように言語仕様を制定するのもコードを書くのも難しいです。 Adaでも細部の仕様はAda 2012、Technical Corrigendum 1、そしてAda 202xと二転三転した部分もあります。 これから説明するものは他に契約プログラミングを実装した言語と挙動が異なる部分も多いです。 標準化委員会が長年に渡って詰めた結果であり、違和感を感じても熟考していただければと思います。 (正直私も違和感がある部分がなくはないです。) そして繰り返しになりますが私の理解がおかしければご指摘いただければ幸いです。 .. container:: gray-and-small Walter先生が深く考えずに実装して後悔しているらしい(?)D言語の挙動はまあ参考にしなくていいとしまして、元祖のEiffelとも異なる部分があります。 そのような事情ですので今回はAda 202xでここが変わったとピンポイントに書くのではなく、全体を見渡す形で説明したいと思います。 class-wide アスペクト --------------------- 契約関係のアスペクトには後ろに ``'Class`` の付いた版があります。 tagged型とそのプリミティブ(同じパッケージで宣言されたサブプログラム、多態の対象になる)にだけ指定できます。 契約が導入される前のAda 2005以前にもストリームにclass-wide型の値を実際の型の情報付きで読み書きするための ``T'Class'Read``/``T'Class'Write`` 属性がありました。 同じように ``'Class`` の付いた版のアスペクトは(基本的に)派生先にも継承されます。 (以降は「``'Class`` の付いた版」のことを「class-wide版」と書きます。) 逆に言えば ``'Class`` の付かない版のアスペクトは(基本的に)その型限りということです。 とはいえアスペクトが継承されなくてもアスペクトによって起こる動作そのものは継承されますから非常にややこしいです。 ``Global'Class`` 、 ``Type_Invariant'Class`` 、 ``Pre'Class`` 、 ``Post'Class`` そして ``Stable_Properties'Class`` が存在します。 ただし ``Stable_Properties'Class`` は継承されません。 後述します。 ですので実際に考える必要があるのは他の4つとなります。 サンプル ++++++++ サンプルのベースを先に書いておきます。 これに各アスペクトを追加していきます。 .. code-block:: ada package Base is type B is tagged limited private; function Create (Value : Integer) return B; function Get_Value (Object : B) return Integer; procedure Set_Value (Object : in out B; Value : in Integer); Time : Integer := 0; Set_Value_Is_Canceled : exception; private type B is tagged limited record E1 : Ineger := 0; Modified_Time : Integer := Time; end record; end Base; .. code-block:: ada package body Base is function Create (Value : Integer) return B is begin return B'(E1 => Value, Modified_Time => Time); end Create; function Get_Value (Object : B) return Integer is begin return Object.E1; end Get_Value; procedure Set_Value (Object : in out B; Value : in Integer); begin Object.E1 := Value; Modified_Time := Time; end Set_Value; end Base; .. code-block:: ada with Base; package Derived is type D is new Base with private; overriding function Create (Value : Integer) return D; overriding function Get_Value (Object : D) return Integer; overriding procedure Set_Value (Object : in out D; Value : in Integer); private type D is new Base with record E2 : Ineger := 0; end record; end Derived; .. code-block:: ada package body Derived is overriding function Create (Value : Integer) return D is begin return D'(Base.Create (0) with E2 => Value); end Create; overriding function Get_Value (Object : D) return Integer is begin return Object.E2; end Get_Value; overriding procedure Set_Value (Object : in out D; Value : in Integer) is begin Object.E2 := Value; end Set_Value; end Derived; Globalと継承 ++++++++++++ ``Global`` はサブプログラムがアクセスするグローバル変数を表明します。 継承されません。 例に追加してみます。 .. code-block:: ada package Base is -- 省略 function Create (Value : Integer) return B with Global => in Time; function Get_Value (Object : B) return Integer with Global => null; procedure Set_Value (Object : in out B; Value : in Integer) with Global => in Time; -- 省略 .. code-block:: ada with Base; package Derived is -- 省略 overriding function Create (Value : Integer) return D with Global => in Time; overriding function Get_Value (Object : D) return Integer with Global => null; overriding procedure Set_Value (Object : in out D; Value : in Integer) with Global => null; -- 省略 ``Base.Create`` とそれを呼び出している ``Derived.Create`` 、そして ``Base.Set_Value`` は ``Time`` に ``in`` アクセスする、それ以外はグローバル変数にはアクセスしない、と、そのまま書きました。 これはそれぞれ普通に呼んでいる分には問題ありません。 .. code-block:: ada with Base; with Derived; procedure Main is begin parallel do declare B_Object : Base.B := Base.Create (1); -- Global => in Time begin Base.Set_Value (B_Object); -- Global => in Time end; and declare D_Object : Derived.D := Derived.Create (2); -- Global => in Time begin Base.Set_Value (D_Object); -- Global => null end; end do; end Main; しかし、このままでは多態呼び出しができなくなります。 .. code-block:: ada with Base; with Derived; procedure Main is begin parallel do declare B_As_Classwide_B : Base.B'Class := Base.Create (1); -- Global => in Time begin Base.Set_Value (B_As_Classwide_B); -- Global => in out all end; and declare D_As_Classwide_B : Base.B'Class := Derived.Create (2); -- Global => in Time begin Base.Set_Value (D_As_Classwide_B); -- error -- Global => in out all end; end do; end Main; 多態呼び出しにおいて派生先ではどのような変数にアクセスしているかわかりませんので ``in out all`` が仮定されてしまいます。 これを解決するためには基底の側に ``Global'Class`` も併せて指定します。 .. code-block:: ada package Base is -- 省略 function Create (Value : Integer) return B with Global => in Time, Global'Class => in Time; function Get_Value (Object : B) return Integer with Global => null, Global'Class => null; procedure Set_Value (Object : in out B; Value : in Integer) with Global => in Time, Global'Class => in Time; -- 省略 .. code-block:: ada with Base; with Derived; procedure Main is begin parallel do declare B_As_Classwide_B : Base.B'Class := Base.Create (1); -- Global => in Time begin Base.Set_Value (B_As_Classwide_B); -- Global => in Time end; and declare D_As_Classwide_B : Base.B'Class := Derived.Create (2); -- Global => in Time begin Base.Set_Value (D_As_Classwide_B); -- Global => in Time end; end do; end Main; ``in`` アクセス同士は衝突しませんので通るようになりました。 ``Global'Class`` は ``overriding`` では変更できません。 そして ``Global`` は ``Global'Class`` の部分集合である必要があります。 デフォルトの ``in out all`` は全ての上位集合ですので指定しなくても通常は問題ありませんが、例のように並列化の中で多態呼び出しに制限ができてしまいます。 Type_Invariantと継承 ++++++++++++++++++++ ``Type_Invariant`` はその型のオブジェクトが常に満たさなければならない不変条件です。 継承されませんが、派生型に埋め込まれている基底型部分では動作します。 基底型 ``Base.B`` に適当な ``Type_Invariant`` を追加してみます。 .. code-block:: ada package Base is type B is tagged limited private with Type_Invariant => Get_Value (B) > 0; -- 省略 この不変条件は、この例の場合ですとデフォルト初期化及び ``Base.Create`` と ``Base.Set_Value`` の最後でチェックされます。 ``Derived.D`` のオブジェクトに影響するのは埋め込まれている ``B`` 部分だけです。 具体的には ``Derived.Create`` の中で ``Base.Create`` を呼んでいる部分だけですね。 ``Derived.Create`` を呼び出したら何が起きるかを見てみます。 .. code-block:: ada with Derived; procedure Main is Object : Derived.D := Derived.Create (1); -- runtime error -- Type_Invariant => Base.Get_Value (Base.B (Object)) > 0 begin null; end Main; 引数は ``1`` ですが ``Derived.Create`` の中では ``Base.Create`` には ``0`` を渡しているため ``Object.E1`` は ``0`` になります。 ``Get_Value`` は ``Derived`` で ``overriding`` していますが不変条件の式中では多態しません。 結果 ``Get_Value`` が ``Object.E1`` を返して不変条件違反で実行時エラーになります。 (多態してしまいますと条件自体を後から変えられることになってしまいます。 この例ですと ``E1`` が ``0`` のインスタンスを作れてしまうことになります。) ``Type_Invariant'Class`` は継承され、派生型の文脈で再解釈されます。 先程の不変条件を ``Type_Invariant'Class`` に変えてみます。 .. code-block:: ada package Base is type B is tagged limited private with Type_Invariant'Class => Get_Value (B) > 0; -- 省略 これは、次のように両方に ``Type_Invariant`` を指定したのと同じ動作になります。 .. code-block:: ada package Base is type B is tagged limited private with Type_Invariant => Get_Value (B) > 0; -- 省略 .. code-block:: ada with Base; package Derived is type D is new Base with private with Type_Invariant => Get_Value (D) > 0; -- 省略 ``Base.B`` の方では ``Base.Get_Value`` が呼ばれ、 ``Derived`` の方では ``Derived.Get_Value`` が呼ばれることになります。 最終的に ``D`` のオブジェクトに対するチェックは ``Base.Get_Value (Base.B (Object)) > 0 and Derived.Get_Value (Object) > 0`` となります。 この場合もやはり実行時エラーになります。 class-wide版の条件内の関数呼び出しは多態せずに両方がチェックされます。 継承階層の途中にabstract型(抽象型ではなくてインスタンスを作れない方)がある場合はabstract型のところだけ飛ばされます。 これは事前条件 ``Pre'Class`` でも事後条件 ``Post'Class`` でも同様です。 元々はclass-wide版の方は式中の関数呼び出しは多態していたのですがTechnical Corrigendum 1で変更されました。 Ada 202xでabstract型は飛ばすようになりました。 どうしても多態したければ、明示的に書けば多態させることもできます。 ``Get_Value (B'Class (B)) > 0`` みたいにclass-wide型にすればいいです。 Preと継承 +++++++++ ``Pre`` はサブプログラムの事前条件です。 継承されませんが、該当サブプログラムが呼び出されれば動作します。 事実上サブプログラムの先頭に埋め込まれるpragma ``Assert`` です。 他とは無関係に評価されます。 ``overriding`` する際に上手く再定義しないとLSPを満たせなくなります。 ``Derived.Set_Value`` に適当な ``Pre`` を追加してみます。 (なお ``Type_Invariant`` の例で追加した不変条件は消しておきます。) .. code-block:: ada with Base; package Derived is -- 省略 overriding procedure Set_Value (Object : in out D; Value : in Integer) with Pre => Value = 0; -- 省略 ``Base.Set_Value`` には事前条件を書いていないため常に成立する ``True`` を仮定するのが妥当です。 そして事前条件は緩めることしか許されていませんが、この ``Value = 0`` はそのルールを破っています。 というわけで ``overriding`` 先に ``Pre`` を使うのは推奨できません。 推奨できないだけで動作を把握していれば色々便利な使い方もありますが…… ``Pre'Class`` は継承され、派生型の文脈で再解釈されます。 先ほどの事前条件を ``Pre'Class`` に変えてみます。 .. code-block:: ada with Base; package Derived is -- 省略 overriding procedure Set_Value (Object : in out D; Value : in Integer) with Pre'Class => Value = 0; -- error -- 省略 これはコンパイルエラーになります。 Technical Corrigendum 1からエラーということになり、元の ``Base.Set_Value`` にも ``Pre'Class`` が必要になりました。 何も書いていない場合は ``True`` を仮定するのが妥当ですが、それで嬉しい場合はまずないですし。 (原則から言えば先程の ``Pre`` も同様にコンパイルエラーでいいはずですが「色々便利な使い方」のために見逃されています。) というわけで ``Base.Set_Value`` にも ``Pre'Class`` を書き足します。 .. code-block:: ada package Base is -- 省略 procedure Set_Value (Object : in out B; Value : in Integer) with Pre'Class => Value > 0; -- 省略 ``Pre'Class`` は条件を緩めることしかできないというルールに沿うため継承したものと論理和が取られます。 ですので ``Derived.Set_Value`` の事前条件は最終的に ``Value > 0 or Value = 0`` となります。 .. code-block:: ada with Base; with Derived; procedure Main is begin Base.Set_Value (Base.Create (1), 100); -- Pre => Value > 0 Derived.Set_Value (Derived.Create (2), 0); -- Pre => Value > 0 or Value = 0 end Main; 注意しないといけないのは事前条件は多態しないということです。 ``Type_Invariant`` で触れましたように事前条件の式の中での呼び出しは多態しません。 それとは別に、事前条件の書かれているサブプログラム自体を多態呼び出ししても事前条件は多態しません。 ``Set_Value`` を多態呼び出ししてみます。 .. code-block:: ada with Base; with Derived; procedure Main is D_As_Classwide_B : Base.B'Class := Derived.Create (2); begin Base.Set_Value (D_As_Classwide_B, 0); -- runtime error -- Pre => Value > 0 end Main; この場合 ``Base.Set_Value`` の ``Pre'Class`` である ``Value > 0`` のみが評価されて実行時エラーになります。 確かに派生先では事前条件を緩めることができますが、アップキャストして基底型として扱っているときは基底型の条件に沿わないとLSPを満たせないからです。 これに関して詳しく説明しようとしますと文章量が必要になりますし、私が説明するよりもAARMの該当箇所を読んでいただいたほうがいいかなと……。 | http://www.ada-auth.org/standards/2xaarm/html/AA-6-1-1.html#p38 ……わかんないですよねー。 私もわかりません。 規格の文面なんて前提知識がないと意味不明です。 えーと、D言語のコンパイラdmdに対するバグ報告からの議論を読んでいただいたほうがわかりやすいと思います。 Meyer先生の「オブジェクト指向入門」の該当箇所も示されています。 | https://issues.dlang.org/show_bug.cgi?id=6857 ちなみにGNATにも同じバグがありましたがgcc 8ぐらいで直りました。 dmdはまだ直ってないようです。 Postと継承 ++++++++++ ``Post`` はサブプログラムの事後条件です。 継承されませんが、該当サブプログラムが呼び出されれば動作します。 事実上サブプログラムの最後に埋め込まれるpragma ``Assert`` です。 呼び出し側にとっては表明されていない隠された事後条件みたいに考えればよいと思います。 実際の返値の値域は表明されたものよりも狭いのですが、呼び出し側はそれに依存することはできない、みたいな。 ``Pre`` と異なりLSPの上で問題はないため使っていいです。 ``Base.Set_Value`` に適当な ``Post`` を追加してみます。 .. code-block:: ada package Base is -- 省略 procedure Set_Value (Object : in out B; Value : in Integer) with Pre'Class => Value > 0, Post => Get_Value (Object) > 0; -- 省略 ``Derived.Set_Value`` の事前条件には(``Pre'Class`` の例で追加した) ``Pre'Class => Value = 0`` があるものとします。 .. code-block:: ada with Base; package Derived is -- 省略 overriding procedure Set_Value (Object : in out D; Value : in Integer) with Pre'Class => Value = 0; -- 省略 そうしますと ``Derived.Set_Value (Object, 0)`` の呼び出しの後は ``Base.Get_Value (Base.B (Object))`` と ``Derived.Get_Value (Object)`` の両方とも結果が ``0`` になりますが ``Base.Set_Value`` の ``Post`` は ``Derived.Set_Value`` には継承されませんので問題にはなりません。 .. code-block:: ada with Base; with Derived; procedure Main is begin Base.Set_Value (Base.Create (1), 100); -- Pre => Value > 0 -- Post => Base.Get_Value (Object) > 0 Derived.Set_Value (Derived.Create (2), 0); -- Pre => Value > 0 or Value = 0 -- Post => True end Main; ``Post'Class`` は継承され、派生型の文脈で再解釈されます。 先程の事後条件を ``Post'Class`` に変更してみます。 .. code-block:: ada package Base is -- 省略 procedure Set_Value (Object : in out B; Value : in Integer) with Pre'Class => Value > 0, Post'Class => Get_Value (Object) > 0; -- 省略 この ``Post'Class`` は ``Derived.Set_Value`` に継承されます。 表明されている事後条件はきつくすることしかできないというルールに沿うため継承したものと論理積が取られます。 .. code-block:: ada with Base; with Derived; procedure Main is begin Base.Set_Value (Base.Create (1), 100); -- Pre => Value > 0 -- Post => Base.Get_Value (Object) > 0 Derived.Set_Value (Derived.Create (2), 0); -- runtime error -- Pre => Value > 0 or Value = 0 -- Post => Base.Get_Value (Object) > 0 -- and Derived.Get_Value (Object) > 0 end Main; 結果、実行時エラーになってしまいました。 元で表明されている事後条件には全ての派生型で考えられる最も緩い条件を指定しなければなりません。 ですのでここでは ``Base.Set_Value`` の ``Post'Class`` を修正します。 .. code-block:: ada package Base is -- 省略 procedure Set_Value (Object : in out B; Value : in Integer) with Pre'Class => Value > 0, Post'Class => Get_Value (Object) >= 0; -- 省略 .. code-block:: ada with Base; with Derived; procedure Main is begin Base.Set_Value (Base.Create (1), 100); -- Pre => Value > 0 -- Post => Base.Get_Value (Object) >= 0 Derived.Set_Value (Derived.Create (2), 0); -- Pre => Value > 0 or Value = 0 -- Post => Base.Get_Value (Object) >= 0 -- and Derived.Get_Value (Object) >= 0 end Main; 事後条件は多態します。 ``Type_Invariant`` で触れましたように事後条件の式の中での呼び出しは多態しません。 それとは別に、事後条件の書かれているサブプログラム自体を多態呼び出しした場合は事後条件も多態します。 事前条件を満たすのが呼び出し側の責任なのに対して、事後条件を満たすのはサブプログラム側の責任でありそれはディスパッチ後のサブプログラム本体に付随するものだからです。 事前条件も事後条件もどちらもきつい方を満たさないといけないという覚え方でいいと思います。 (雑。) 上記以外で影響するアスペクト ---------------------------- ``Stable_Properties`` も含めて軽く触れていきます。 Stable_Propertiesと継承 +++++++++++++++++++++++ ``Stable_Properties`` は各プリミティブの ``Post`` として展開され、派生先には継承されません。 ``Stable_Properties'Class`` は各プリミティブの ``Post'Class`` として展開され、派生先には継承されません。 展開された ``Post'Class`` 自体は派生先に継承されます。 ややこしいです。 このような仕様ですので ``Stable_Properties'Class`` を使っている基底型から派生した際、追加したプリミティブに基底型から継承したプリミティブと同様の事後条件を与えるためには ``Stable_Properties'Class`` を繰り返し指定する必要があります。 仮に継承したら、あるいは同じものを指定したらしたで、同じ条件が何度も重複して追加されていく形になって非効率になる恐れがあります。 継承されない仕様になった理由だそうです。 練り込み不足を感じます……。 Default_Initial_Conditionと継承 +++++++++++++++++++++++++++++++ デフォルト初期化の事後条件 ``Default_Initial_Condition`` にはclass-wide版はありません。 継承はされませんが派生型のオブジェクトに埋め込まれている基底型部分では動作します。 aggregate式の基底型部分等も含めてもしデフォルト初期化を使ったら基底型の ``Default_Initial_Condition`` がチェックされますし、基底型部分にデフォルト初期化を使わなければ関係ないです。 例えば ``Base.B`` に常に失敗する ``Default_Initial_Condition`` を書き足したとします。 .. code-block:: ada package Base is type B is tagged limited private with Default_Initial_Condition => False; しかし ``Derived.Create`` は基底部分は ``Base.Create`` を使って作成していますので関係ないです。 .. code-block:: ada package body Derived is overriding function Create (Value : Integer) return D is begin return D'(Base.Create (0) with E2 => Value); end Create; -- 省略 次のように書き換えますと ``Base.B`` のデフォルト初期化となり ``Default_Initial_Condition`` もチェックされます。 (多分。 自信ないです。) .. code-block:: ada package body Derived is overriding function Create (Value : Integer) return D is begin return D'(Base.B with E2 => Value); -- runtime error end Create; -- 省略 Nonblockingと継承 +++++++++++++++++ サブプログラムやRAIIがブロッキングするかどうかを指定する ``Nonblocking`` にはclass-wide版はありませんが、派生先に継承されます。 ``overriding`` によって ``Nonblocking`` かどうかを変えることはできません。 .. |ZWSP| unicode:: U+200B .. ZERO WIDTH SPACE :trim: Static_Predicate |ZWSP| /Dynamic_Predicateと継承 ++++++++++++++++++++++++++++++++++++++++++++++++ ``Type_Invariant`` と同様に動作します。 .. container:: strike …… ``Dynamic_Predicate`` と ``Type_Invariant`` って何が違うのでしょうか。 ……えーと、えーと、そうです。 ``Dynamic_Predicate`` は ``subtype`` にも追加できます。 ……えーと、えーと、他には……。 .. container:: inserted 不変条件はサブプログラムの出口でチェックされます。 predicateは型変換や引数等の入り口側でのチェックが主になります。 関連AI ------ - `AI12-0170-1`_ **Abstract subprogram calls in class-wide precondition expressions** - `AI12-0195-1`_ **Inheriting body but overriding precondition or postcondition** - `AI12-0199-1`_ **Abstract subprogram calls in class-wide invariant expressions** Technical Corrigendum 1で適用済みのものは含めていません。 所感 ---- あたまいたい。 もっと自然な例を用意したい。 明らかに分量配分がおかしい。 ともかく、これで最大の難所は越えたはず……。 ``Pre`` は理屈の上では問題ありですが実用上は ``overriding`` と ``Pre`` が一緒になっているとまずいと気付けそうですので気にしなくていいのではと思います。 ``Stable_Properties'Class`` は普通にプロパティを宣言するようなイメージで使えれば良かったのですが。 EVEのmodelは多分そんな感じで使えますよね。 まあAdaで何層も継承するプログラムを書くほうがどうかしてるとは言えるはず? よく言われますように継承階層はabstract型や ``interface`` と実装との2層に留めましょう。 ``generic`` を多用しましょう。 .. _`AI12-0170-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0170-1.txt .. _`AI12-0195-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0195-1.txt .. _`AI12-0199-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0199-1.txt