Ada 202x (25日目) - 契約と高階関数
==================================

.. post:: Dec 25, 2019
   :tags: ada, ada_2022

普通の日。

経緯
----

契約の静的解析のためには高階関数の仮引数の側にも事前条件や事後条件を書けるようにする必要があります。

例えば、引数で渡された関数に固定の引数を渡すパッケージがあるとします。

.. code-block:: ada

 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;

.. code-block:: ada

 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;

.. code-block:: ada

 generic
    with function Divide (X, Y : Float) return Float;
 package Pkg2 is
    function Invoke return Float;
 end Pkg2;

.. code-block:: ada

 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`` の実装が渡された場合、当然ですが実行時エラーになります。

.. code-block:: ada

 function Divide (X, Y : Float) return Float
   with Pre => Y /= 0.0;

.. code-block:: ada

 function Divide (X, Y : Float) return Float is
 begin
    return X / Y;
 end Divide;

.. code-block:: ada

 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`` の仮引数に事前条件と事後条件を書けるようになりました。

.. code-block:: ada

 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;

.. code-block:: ada

 generic
    with function Divide (X, Y : Float) return Float
      with Pre => Y /= 0.0;
 package Pkg2 is
    function Invoke return Float;
 end Pkg2;

注意としまして、実引数との条件の矛盾を調べるのは検証器の仕事となります。
あくまでAdaの範囲では事前条件と事後条件は動的なチェックですので条件自体の矛盾のチェックも行われません。

実行時には仮引数と実引数の両方の条件が評価されます。
議論の上ではラッパーとして例えられました。

このようなイメージでしょうか。

.. code-block:: 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;

.. code-block:: ada

 -- 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**

.. _`AI12-0220-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0220-1.txt
.. _`AI12-0272-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0272-1.txt