Ada 202x (26日目) - 契約と継承¶

一番理解も説明も難しいところが来てしまいました……。怪しい箇所がありましたらご指摘ください。遠慮なく。ええもう本当に。

リスコフの置換原則¶

継承で大事なことはリスコフの置換原則(Liskov substitution principle、LSP)を守ることです。基底型の性質は全て派生型で満たされなければならない(置換可能性)というやつです。

しかし実際にこれを守るのは非常に難しいです。理解するのも問題のないように言語仕様を制定するのもコードを書くのも難しいです。 Adaでも細部の仕様はAda 2012、Technical Corrigendum 1、そしてAda 202xと二転三転した部分もあります。

これから説明するものは他に契約プログラミングを実装した言語と挙動が異なる部分も多いです。標準化委員会が長年に渡って詰めた結果であり、違和感を感じても熟考していただければと思います。 (正直私も違和感がある部分がなくはないです。)

そして繰り返しになりますが私の理解がおかしければご指摘いただければ幸いです。

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つとなります。

サンプル¶

サンプルのベースを先に書いておきます。これに各アスペクトを追加していきます。

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;

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;

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;

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 はサブプログラムがアクセスするグローバル変数を表明します。継承されません。

例に追加してみます。

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;
   -- 省略

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 アクセスする、それ以外はグローバル変数にはアクセスしない、と、そのまま書きました。

これはそれぞれ普通に呼んでいる分には問題ありません。

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;

しかし、このままでは多態呼び出しができなくなります。

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 も併せて指定します。

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;
   -- 省略

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 を追加してみます。

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 を呼び出したら何が起きるかを見てみます。

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 に変えてみます。

package Base is
   type B is tagged limited private
     with Type_Invariant'Class => Get_Value (B) > 0;
   -- 省略

これは、次のように両方に Type_Invariant を指定したのと同じ動作になります。

package Base is
   type B is tagged limited private
     with Type_Invariant => Get_Value (B) > 0;
   -- 省略

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 の例で追加した不変条件は消しておきます。)

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 に変えてみます。

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 を書き足します。

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 となります。

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 を多態呼び出ししてみます。

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 を追加してみます。

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 があるものとします。

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 には継承されませんので問題にはなりません。

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 に変更してみます。

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 に継承されます。

表明されている事後条件はきつくすることしかできないというルールに沿うため継承したものと論理積が取られます。

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 を修正します。

package Base is
   -- 省略
   procedure Set_Value (Object : in out B; Value : in Integer)
     with
       Pre'Class  => Value > 0,
       Post'Class => Get_Value (Object) >= 0;
   -- 省略

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 を書き足したとします。

package Base is
   type B is tagged limited private
     with Default_Initial_Condition => False;

しかし Derived.Create は基底部分は Base.Create を使って作成していますので関係ないです。

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 もチェックされます。 (多分。自信ないです。)

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 かどうかを変えることはできません。

Static_Predicate/Dynamic_Predicateと継承¶

Type_Invariant と同様に動作します。

…… Dynamic_Predicate と Type_Invariant って何が違うのでしょうか。

……えーと、えーと、そうです。 Dynamic_Predicate は subtype にも追加できます。 ……えーと、えーと、他には……。

不変条件はサブプログラムの出口でチェックされます。 predicateは型変換や引数等の入り口側でのチェックが主になります。

所感¶

あたまいたい。

もっと自然な例を用意したい。

明らかに分量配分がおかしい。

ともかく、これで最大の難所は越えたはず……。

Pre は理屈の上では問題ありですが実用上は overriding と Pre が一緒になっているとまずいと気付けそうですので気にしなくていいのではと思います。

Stable_Properties'Class は普通にプロパティを宣言するようなイメージで使えれば良かったのですが。 EVEのmodelは多分そんな感じで使えますよね。まあAdaで何層も継承するプログラムを書くほうがどうかしてるとは言えるはず？よく言われますように継承階層はabstract型や interface と実装との2層に留めましょう。 generic を多用しましょう。

Previous: Ada 202x (25日目) - 契約と高階関数 Next: Ada 202x (27日目) - Iterator_View

Ada 202x (26日目) - 契約と継承¶

リスコフの置換原則¶

class-wide アスペクト¶

サンプル¶

Globalと継承¶

Type_Invariantと継承¶

Preと継承¶

Postと継承¶

上記以外で影響するアスペクト¶

Stable_Propertiesと継承¶

Default_Initial_Conditionと継承¶

Nonblockingと継承¶

Static_Predicate/Dynamic_Predicateと継承¶

関連AI¶

所感¶

Whenever construction in my heart!

2019-12-26(Thu)

Recent Posts

Tags

Archives

Ada 202x (26日目) - 契約と継承¶

リスコフの置換原則¶

class-wide アスペクト¶

サンプル¶

Globalと継承¶

Type_Invariantと継承¶

Preと継承¶

Postと継承¶

上記以外で影響するアスペクト¶

Stable_Propertiesと継承¶

Default_Initial_Conditionと継承¶

Nonblockingと継承¶

Static_Predicate​/Dynamic_Predicateと継承¶

関連AI¶

所感¶

Static_Predicate/Dynamic_Predicateと継承¶