Ada 202x (25日目) - 契約と高階関数¶
普通の日。
経緯¶
契約の静的解析のためには高階関数の仮引数の側にも事前条件や事後条件を書けるようにする必要があります。
例えば、引数で渡された関数に固定の引数を渡すパッケージがあるとします。
package Pkg1 is
type Divide_Access is access function (X, Y : Float) return Float;
function Invoke (Divide : not null Divide_Access) return Float;
end Pkg1;
package body Pkg1 is
function Invoke (Divide : not null Divide_Access) return Float is
begin
return Divide (0.0, 0.0);
end Invoke;
end Pkg1;
generic
with function Divide (X, Y : Float) return Float;
package Pkg2 is
function Invoke return Float;
end Pkg2;
package body Pkg2 is
function Invoke return Float is
begin
return Divide (0.0, 0.0);
end Invoke;
end Pkg2;
これらのパッケージの引数 Divide に対して次のような 0.0 ではない Y を要求する Divide の実装が渡された場合、当然ですが実行時エラーになります。
function Divide (X, Y : Float) return Float
with Pre => Y /= 0.0;
function Divide (X, Y : Float) return Float is
begin
return X / Y;
end Divide;
with Pkg_1;
with Divide;
procedure Main is
package Pkg2_Instance is new Pkg2 (Divide);
Z : Float;
begin
Z := Pkg1.Invoke (Divide'Access); -- runtime error
Z := Pkg2_Instance.Invoke; -- runtime error
end Main;
しかし検証器は Pkg1 や Pkg2 それぞれを別々に解析している分にはこれを検出できません。
というよりは別々に解析している限りは検出できないのが正しいです。
Divide というそれらしい名前を付けていますが Y => 0.0 を渡しても構わない実装を与えることもできますし。
しかし意図としましては割り算ですので Y => 0.0 はエラーとして検出したいわけです。
これまでは仮引数に事前条件や事後条件を書けませんでしたのでこのような意図を伝えることができませんでした。
Ada 202xでの改善¶
access型や generic の仮引数に事前条件と事後条件を書けるようになりました。
package Pkg1 is
type Divide_Access is access function (X, Y : Float) return Float
with Pre => Y /= 0.0;
function Invoke (Divide : not null Divide_Access) return Float;
end Pkg1;
generic
with function Divide (X, Y : Float) return Float
with Pre => Y /= 0.0;
package Pkg2 is
function Invoke return Float;
end Pkg2;
注意としまして、実引数との条件の矛盾を調べるのは検証器の仕事となります。 あくまでAdaの範囲では事前条件と事後条件は動的なチェックですので条件自体の矛盾のチェックも行われません。
実行時には仮引数と実引数の両方の条件が評価されます。 議論の上ではラッパーとして例えられました。
このようなイメージでしょうか。
-- This is an image!
package body Pkg1 is
function Invoke (Divide : not null Divide_Access) return Float is
function Divide_Wrapper (X, Y : Float) return Float
with Pre =>Y /= 0 is
begin
return Divide (X, Y);
end Divide_Wrapper;
begin
return Divide_Wrapper (0.0, 0.0);
end Invoke;
end Pkg1;
-- This is an image!
package body Pkg2 is
function Invoke return Float is
function Divide_Wrapper (X, Y : Float) return Float
with Pre => Y /= 0 is
begin
return Divide (X, Y);
end Divide_Wrapper;
begin
return Divide_Wrapper (0.0, 0.0);
end Invoke;
end Pkg2;
デフォルト初期化の事後条件である Default_Initial_Condition も generic の仮引数側の型に書くことができるようになっています。
関連AI¶
AI12-0220-1 Pre/Post for access-to-subprogram types
AI12-0272-1 Contracts for generic formal parameters