如何在 procedure/funtion 的 Pre/Post 合同中访问程序的参数，该程序将程序作为访问参数？

Question

Containers.Vector 包定义了一些过程，这些过程可以访问过程作为参数。本程序支持一个参数。

示例：

procedure Update_Element
  (Container : in out Vector;
   Index     : in     Index_Type;
   Process   : not null access procedure (E : in out Element_Type));

procedure Query_Element
  (Container : in Vector;
   Index     : in Index_Type;
   Process   : not null access procedure (E : in Element_Type));

是否可以在程序 Query_Element 和 Update_Element 的 Pre 和 Post 合同中使用 E？

写这样的东西：

procedure Update_Element
  (Container : in out Vector;
   Index     : in     Index_Type;
   Process   : not null access procedure (E : in out Element_Type))
with Post => Element(Container,Index) = E;

结果编译错误："E" is undefined

如果可能，解决方案应与 Spark 兼容。

Answer 1

据我所知，Ada (2012) 的当前标准不允许在子程序指针上有契约。它将在下一个 Ada 标准版本（目前称为 202x）中被允许。有关它的更多信息，以及示例：

https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#contracts-for-subprogram-pointers

如何在 procedure/funtion 的 Pre/Post 合同中访问程序的参数，该程序将程序作为访问参数？

How to access a parameter of a procedure in Pre/Post contracts of a procedure/funtion that has the the procedure as access parameter?

ada

spark-ada