Ada 202x (39日目) - その他の契約関連の変更 ========================================== .. post:: Jan 08, 2020 :tags: ada, ada_2022 ここに書いているのはあくまで現時点での情報です。 確定ではありません。 今後変わる恐れもあります。 実際変わりそうです。 (今更。) 標準ライブラリの事後条件 ------------------------ Ada 202xでは標準ライブラリの多くに事前条件/事後条件が追加されました。 うち事後条件は失敗することはなく ``Assertion_Error`` を発生させないと明確に規定されました。 標準ライブラリの事後条件は動作を示す説明のために追加されています。 標準ライブラリの事前条件は勿論違反した引数を渡すことで失敗します。 (pragma ``Assertion_Policy`` ではなく)pragma ``Suppress`` で抑制できます。 :doc:`37日目 `\ を参照。 'Old属性の制限緩和 ------------------ 事後条件の中でサブプログラムの実行前の値を参照できる ``'Old`` 属性が使いやすくなりました。 ``'Old`` 属性の動作として最初に値を保存しなけれななりません。 そのため短絡評価等によって評価されるかどうかわからない箇所では使用できません。 値を保存しようとするアクセス自体がエラーを引き起こす恐れがあるからです。 .. code-block:: ada 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`` を保存するためには ``Index`` が ``X`` の範囲内である必要があります。 ``X`` は ``in out`` パラメータですので式 ``Index in X.First_Index .. X.Last_Index`` の結果は実行の前後で変化する恐れがあります。 そのため実行前に ``X (Index)`` にアクセスしてよいかどうかわからないためエラーになります。 Ada 2012では評価されないかもしれない式の中では一律駄目だったのですが、Ada 202xで緩和されて実行前に条件が確定できるなら ``'Old`` 属性が使えるようになりました。 この例では ``First_Index`` と ``Last_Index`` も実行前の値を使うことで ``X (Index)`` にアクセスしてよいかどうかを確定できます。 ついでに ``X`` の長さが変わらないことも表明してしまいましょう。 条件を続けるために ``and then`` を使いますとこれも短絡評価になってしまいますので ``and`` を使います。 .. code-block:: ada 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アスペクト ------------------------------- ``task`` や ``protected`` では ``Pre'Class`` 等のclass-wide版アスペクトは使えないことが確定しました。 ``interface`` から継承することはできます。 ``task`` や ``protected`` は言わばfinalでそこから更に派生することはできませんのでほぼ問題はないと思います。 ただ継承した ``Pre'Class`` を緩めたいときがもしあれば困るかもですね。 (そもそも ``synchronized interface`` 自体ほとんど使われてなさそうな。) protectedと外部呼び出し ----------------------- 型に付けるアスペクトの式の中では自身のオブジェクトは型名で表します。 .. code-block:: ada type R is record Component : Integer; end record with Type_Invariant => R.Component > 0; この ``Type_Invariant`` の式中の ``R`` は他言語で言う ``Self`` や ``Current`` や ``this`` の意味です。 直接要素を参照することはできません。 .. code-block:: ada type R is record Component : Integer; end record with Type_Invariant => Component > 0; -- error ですが ``protected`` の場合は直接参照するかオブジェクト名から ``.`` で続けるかで意味が変わってしまいます。 .. code-block:: ada protected type P1 with Type_Invariant => P.Read > 0 is -- external call function Read return Integer; end P; オブジェクト名から続けた場合は外部呼び出しとして同期が行われます。 契約の中では同期したくありませんので内部呼び出しのために直接 ``Read`` とだけ書きたいのですがエラーになってしまっていました。 .. code-block:: ada protected type P1 with Type_Invariant => Read > 0 is function Read return Integer; end P; Ada 202xでは ``protected`` の要素はアスペクト中でも内部呼び出しできるようになりました。 また逆の話で、デフォルト引数と事前条件では内部呼び出しが禁止されました。 デフォルト引数や事前条件は同期前に評価されるためです。 .. code-block:: ada 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** .. _`AI12-0166-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0166-1.txt .. _`AI12-0179-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0179-1.txt .. _`AI12-0180-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0180-1.txt .. _`AI12-0182-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0182-1.txt .. _`AI12-0198-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0198-1.txt .. _`AI12-0217-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0217-1.txt .. _`AI12-0280-2`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0280-2.txt