Ada 202x (5日目) - delta aggregate¶
そろそろ疲れが出てきました。 簡単なので済ませます。
経緯¶
SPARKという、Adaのサブセットに静的な検証機能を追加したAdaCore社の製品がありまして。 そのSPARKでは様々な条件を式として書く必要があります。
type Rect is record
Left, Right, Top, Bottom : Float;
end record;
というようなrecordがあるとして、この型のオブジェクトの一部分だけを変更したいとします。
procedure Set_Left (X : in out Rect; New_Left : in Float) is
begin
X.Left := New_Left;
end Set_Left;
このサブプログラムに検証のための事後条件を書き足します。
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ですと、こう書けます。
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ですと元の値が { } の外に来ます。
x == old_x {left = new_left}
というわけでSPARKにもこの機能が独自に追加されました。
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 を再利用した構文です。
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