Ada 202x (39日目) - その他の契約関連の変更¶
ここに書いているのはあくまで現時点での情報です。 確定ではありません。 今後変わる恐れもあります。 実際変わりそうです。 (今更。)
標準ライブラリの事後条件¶
Ada 202xでは標準ライブラリの多くに事前条件/事後条件が追加されました。
うち事後条件は失敗することはなく 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 を保存するためには 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 を使います。
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と外部呼び出し¶
型に付けるアスペクトの式の中では自身のオブジェクトは型名で表します。
type R is
record
Component : Integer;
end record
with Type_Invariant => R.Component > 0;
この Type_Invariant の式中の R は他言語で言う Self や Current や this の意味です。
直接要素を参照することはできません。
type R is
record
Component : Integer;
end record
with Type_Invariant => Component > 0; -- error
ですが protected の場合は直接参照するかオブジェクト名から . で続けるかで意味が変わってしまいます。
protected type P1 with Type_Invariant => P1.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 202xでは 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