Procedure ran in Spark?

General
1

Is there a simple way of asking Spark/gnatprove to tell me if a particular procedure has not been ran exactly once before returning?

E.g,
Register at start

De-register called exactly once on all paths?

2

Maybe I could abuse an unitialised variable but not sure if that would be problematic :thinking:

4

Here is a stupid idea…

But maybe the procedure could change a value to True (for example Proc_Ran := True;) and then you can require that SPARK prove that for all exit conditions of a function or whatever, Proc_Ran = True

5

Thank you. That may be a good option though it might complain about it not being used. Also wondering if the Ada double begin trick or the gnat extension would work. My runtime doesn’t have finalization.

Update: The begin trick works with exceptions but seemingly not with return. The finally extension might work but not sure I want to use experimental.

7

Enter Ghost Code.
IIUC, this is exactly the sort of stuff ghost code was intended for.
I haven’t used it, but I’d assume that you would just throw Ghost aspect on a Natural, increment that variable in all the functions that are required-but-mutually-exclusive, and then put the Post => Operation_Count = 1 annotation on your ‘main’ subprogram.

(Note: With GNAT, you can have an ads file for your “main”, and then you prove SPARK there.)

3 Likes
8

I did something similar but without ghost code but you’re absolutely right. Time to read up on Ghost code.

9

This didn’t really work out as I want it at library level and covering a corner case would be a bit clunky. I shall just wait for finally to land, apparently potentially with Gnat 16.