Ada 202x (5日目) - delta aggregate
==================================

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

そろそろ疲れが出てきました。
簡単なので済ませます。

経緯
----

SPARKという、Adaのサブセットに静的な検証機能を追加したAdaCore社の製品がありまして。
そのSPARKでは様々な条件を式として書く必要があります。

.. code-block:: ada

 type Rect is record
    Left, Right, Top, Bottom : Float;
 end record;

というようなrecordがあるとして、この型のオブジェクトの一部分だけを変更したいとします。

.. code-block:: ada

 procedure Set_Left (X : in out Rect; New_Left : in Float) is
 begin
    X.Left := New_Left;
 end Set_Left;

このサブプログラムに検証のための事後条件を書き足します。

.. code-block:: ada

 procedure Set_Left (X : in out Rect; New_Left : in Float)
   with Post =>
     X.Left = New_Left and X.Right = X'Old.Right
       and then X.Top = X'Old.Top and then X.Bottom = X'Old.Bottom;

最初の ``and`` が ``and then`` ではないのはその前の条件中の ``X.Left`` がサブプログラム実行後の値を参照しているため短絡評価にしてしまうと実行前に ``'Old`` を保存していいかわからなくなるからです。
無条件に保存すれば良いと思われるかもしれませんが場合によっては例外になるかもしれない式(配列の範囲外アクセス等)に ``'Old`` が付けられているかもしれませんのでなるべく保存しないような仕様になっています。

ちなみにこの ``Post`` の構文はAda 2012にも採用されています。
SPARKですと静的に検証されますが、Adaとしての動作は実行時の検証となります。

それで、まあ、やってられませんね。
この例では ``Rect`` ですからまずありえませんけれども、もし要素数が増えたら漏れが出そうです。

そうなると必要になるのが、関数型言語にある構造体の一部を更新する式です。
例えばOCamlですと、こう書けます。

.. code-block:: ocaml

 type rect = {
   mutable left: float;
   mutable right: float;
   mutable top: float;
   mutable bottom: float};;
 
 let set_left (x: rect) (new_left: float) = x.left <- new_left;;
 
 (* OCamlには検証の機能はないため実際に動かして確認 *)
 let x = {left = 1.0; right = 2.0; top = 3.0; bottom = 4.0};;
 let old_x = (Obj.obj (Obj.dup (Obj.repr x)): rect);; (* clone *)
 set_left x 5.0;;
 assert (x = {old_x with left = 5.0});; (* このwith構文です *)

Haskellですと元の値が ``{`` ``}`` の外に来ます。

.. code-block:: haskell

 x == old_x {left = new_left}

というわけでSPARKにもこの機能が独自に追加されました。

.. code-block:: ada

 procedure Set_Left (X : in out Rect; New_Left : in Float)
   with Post =>
     X = X'Old'Update (Left => New_Left);

この構文がAda 202xにも提案されましたが却下されました。
これは見ての通り属性の構文を流用したものです。
Adaでは属性は関数の形を取るようになっていて、可変パラメータな上に配列の場合は数値や範囲を取れさえもするこの ``'Update`` は馴染まないとかなんとか。

Ada 202xでの改善
----------------

代わりに提案されたのが予約語 ``delta`` を再利用した構文です。

.. code-block:: ada

 procedure Set_Left (X : in out Rect; New_Left : in Float)
   with Post =>
     X = (X'Old with delta Left => New_Left);

元の値が括弧の中だからOCaml派！
というわけではなく、Adaには元々、基底型の値に派生型の要素を追加して派生型の値を作るextension aggregateという機能がありましたので、それに倣った形です。

``delta`` は固定小数点数の刻み幅に使われていた予約語です。
Adaではたまにこういう予約語の再利用があります。

関連AI
------

- `AI12-0127-1`_ **Partial aggregate notation**

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