ada - 如何在将过程作为访问参数的过程/函数的前/后契约(Contract)中访问过程的参数？

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