Ada 2020 (39日目) - その他の契約関連の変更

ここに書いているのはあくまで現時点での情報です。 確定ではありません。 今後変わる恐れもあります。 実際変わりそうです。 (今更。)

標準ライブラリの事後条件

Ada 2020では標準ライブラリの多くに事前条件/事後条件が追加されました。

うち事後条件は失敗することはなく Assertion_Error を発生させないと明確に規定されました。 標準ライブラリの事後条件は動作を示す説明のために追加されています。

標準ライブラリの事前条件は勿論違反した引数を渡すことで失敗します。 (pragma Assertion_Policy ではなく)pragma Suppress で抑制できます。 37日目を参照。

‘Old属性の制限緩和

事後条件の中でサブプログラムの実行前の値を参照できる 'Old 属性が使いやすくなりました。

'Old 属性の動作として最初に値を保存しなけれななりません。 そのため短絡評価等によって評価されるかどうかわからない箇所では使用できません。 値を保存しようとするアクセス自体がエラーを引き起こす恐れがあるからです。

package Float_Vectors is new Ada.Containers.Vectors (Positive, Float);

procedure Increment (X : in out Float_Vectors.Vector; Index : in Integer)
  with Post =>
    (if Index in X.First_Index .. X.Last_Index then
       X (Index) = X (Index)'Old + 1.0) is -- error
begin
   if Index in X.First_Index .. X.Last_Index then
      X (Index) := X (Index) + 1.0;
   end if;
end Increment;

この例では X (Index)'Old を保存するためには IndexX の範囲内である必要があります。 Xin out パラメータですので式 Index in X.First_Index .. X.Last_Index の結果は実行の前後で変化する恐れがあります。 そのため実行前に X (Index) にアクセスしてよいかどうかわからないためエラーになります。

Ada 2012では評価されないかもしれない式の中では一律駄目だったのですが、2020で緩和されて実行前に条件が確定できるなら 'Old 属性が使えるようになりました。

この例では First_IndexLast_Index も実行前の値を使うことで X (Index) にアクセスしてよいかどうかを確定できます。

ついでに X の長さが変わらないことも表明してしまいましょう。 条件を続けるために and then を使いますとこれも短絡評価になってしまいますので and を使います。

procedure Increment (X : in out Float_Vectors.Vector; Index : in Integer)
  with Post =>
    (if Index in X.First_Index'Old .. X.Last_Index'Old then
       X (Index) = X (Index)'Old + 1.0)
      and X.Length = X.Length'Old is
begin
   if Index in X.First_Index .. X.Last_Index then
      X (Index) := X (Index) + 1.0;
   end if;
end Increment;

protectedとclass-wideアスペクト

taskprotected では Pre'Class 等のclass-wide版アスペクトは使えないことが確定しました。 interface から継承することはできます。

taskprotected は言わばfinalでそこから更に派生することはできませんのでほぼ問題はないと思います。 ただ継承した Pre'Class を緩めたいときがもしあれば困るかもですね。 (そもそも synchronized interface 自体ほとんど使われてなさそうな。)

protectedと外部呼び出し

型に付けるアスペクトの式の中では自身のオブジェクトは型名で表します。

type R is
   record
      Component : Integer;
   end record
     with Type_Invariant => R.Component > 0;

この Type_Invariant の式中の R は他言語で言う SelfCurrentthis の意味です。

直接要素を参照することはできません。

type R is
   record
      Component : Integer;
   end record
     with Type_Invariant => Component > 0; -- error

ですが protected の場合は直接参照するかオブジェクト名から . で続けるかで意味が変わってしまいます。

protected type P1 with Type_Invariant => P.Read > 0 is -- external call
   function Read return Integer;
end P;

オブジェクト名から続けた場合は外部呼び出しとして同期が行われます。 契約の中では同期したくありませんので内部呼び出しのために直接 Read とだけ書きたいのですがエラーになってしまっていました。

protected type P1 with Type_Invariant => Read > 0 is
   function Read return Integer;
end P;

Ada 2020では protected の要素はアスペクト中でも内部呼び出しできるようになりました。

また逆の話で、デフォルト引数と事前条件では内部呼び出しが禁止されました。 デフォルト引数や事前条件は同期前に評価されるためです。

protected type P2 is
   function Read return Integer;
   entry Ent1 (X : Integer := Read) -- error
     with Pre => Read > 0;         -- error
end P;

かといって意図しない同期が行われてしまう外部呼び出しも書くべきではないでしょう。

関連AI

  • AI12-0166-1 External calls to protected functions that appear to be internal calls

  • AI12-0179-1 Failure of postconditions of language-defined units

  • AI12-0180-1 Using protected subprograms and entries within an invariant

  • AI12-0182-1 Pre’Class and protected operations

  • AI12-0198-1 Potentially unevaluated components of array aggregates

  • AI12-0217-1 Rules regarding restrictions on the use of the Old attribute are too strict

  • AI12-0280-2 Making ‘Old more flexible