3

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));

是否可以在程序的E前后合同中使用？Query_ElementUpdate_Element

写类似：

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 兼容。

4

1 回答 1

2

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

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

于 2021-10-13T15:48:56.643 回答