如何在Containers.Vector过程的Pre/Post契约中引用传入访问过程的形参

直接在Update_Element、Query_Element的顶层Pre/Post契约中引用子过程形参E是不可行的，E的作用域仅属于传入的Process访问过程的内部定义范围，对外层过程的契约不可见，因此会触发"E" is undefined的编译错误。

SPARK支持为访问子过程类型附加契约，你可以将原本要写在外层契约中对E的约束，转移到自定义的访问过程类型的契约上，即可实现等价的校验效果：

1. 首先定义带契约的访问过程类型，将对E的约束写在该类型的契约中：

-- 对应Update_Element使用的带契约访问过程类型
type Access_Update_Process is not null access procedure
  (E : in out Element_Type)
  with
    -- 可在此处编写E需要满足的前置校验条件
    Pre => E'Valid,
    -- 可在此处编写E被修改后的后置校验条件，按需替换为实际业务逻辑
    Post => E = <你期望的修改后值规则>;

-- 对应Query_Element使用的带契约访问过程类型
type Access_Query_Process is not null access procedure
  (E : in Element_Type)
  with
    Pre => E'Valid;

2. 将外层过程的Process参数替换为上述自定义类型：

procedure Update_Element
  (Container : in out Vector;
   Index     : in     Index_Type;
   Process   : not null Access_Update_Process);

procedure Query_Element
  (Container : in Vector;
   Index     : in Index_Type;
   Process   : not null Access_Query_Process);

验证逻辑说明 #

SPARK会自动完成以下校验，完全覆盖原本的需求：

• 所有传入Update_Element/Query_Element的Process实例，都符合对应访问过程类型的契约要求
• 调用Process时传入的实参（即容器对应索引的元素）满足Process的前置条件
• Process执行完成后，E的后置条件成立，对应容器内的元素状态自然满足约束

如果需要进一步保证Process无额外副作用，可在访问过程类型的契约中附加Global => null、Depends等SPARK标准契约约束即可。

内容的提问来源于stack exchange，提问作者mhatzl