The Containers.Vector package defines some procedures that have an access to a procedure as parameter. This procedure supports one parameter.
Examples:
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));
Is it somehow possible to use E in the Pre and Post contracts of the procedures Query_Element and Update_Element?
Writing something like:
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;
Results in compilation error: "E" is undefined
If possible, the solution should be compatible with Spark.
The current standard of Ada (2012), as far I know, doesn't allow having contracts on subprogram pointers. It will be allowed in the next Ada standard version (currently called 202x). More information about it, with examples: