3

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.

mhatzl
  • 173
  • 1
  • 7
  • That’s not what `Update_Element` does - you’re thinking of `Replace_Element`. Anyway, shouldn’t you be specifying the behaviour of your actual `Process`? – Simon Wright Oct 13 '21 at 14:38
  • 1
    In SPARK, you can't use standard `Ada.Containers.Vectors`. You have to use `Ada.Containers.Formal_Vectors` and other similar formal containers. And they don't have `Update_Element` and `Replace_Element` subprograms. Thus, we can't provide a solution compatible with SPARK. – thindil Oct 13 '21 at 15:15
  • 1
    You are right that `Ada.Containers.Vectors` is not in Spark (should have mentioned that myself, sorry), I just used those procedures as examples to describe what I would like to do. If I do not have access to `E` for the Post contract of `Update_Element`, how could one proof that E got updated? Or is this not needed if `Process` has correct Post conditions as mentioned by @SimonWright. – mhatzl Oct 14 '21 at 12:20
  • 1
    @mhatzl, as mentioned in the answer, at this moment you can't. In Ada202x, it will be at access function type declaration. I' not sure, but maybe the newest version of SPARK allow this with `-gnatX` switch enabled. – thindil Oct 15 '21 at 05:32

1 Answers1

2

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:

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

thindil
  • 881
  • 5
  • 9