Why is Always_Terminates not transitive for access to subprograms?

General
1

I made a mapped table of function pointers in SPARK.

I’ve noticed that the prover understands some aspects applied to a subprogram access type. I can take this basic type:

type Op_Procedure is access procedure (Target : in out Machine);

and then apply preconditions I want maintained, and the prover correctly understands these preconditions:

type Op_Procedure is access procedure (Target : in out Machine)
with Pre => Is_Running (Target);

I get this error if I use a subprogram access in an Always_Terminates subprogram:

machines.adb:44:34: medium: aspect Always_Terminates on "Execute" could be incorrect, call via access-to-subprogram might be nonterminating
   44 |         Builtin_Procedures (Op).all (Self);
      |         ~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~

However, I am not allowed to apply Always_Terminates to an access to subprogram the way that I can apply Pre.

machines.ads:100:35: error: incorrect placement of aspect "Always_Terminates"
  100 |   with Pre => Is_Running (Target), Always_Terminates;
      |                                  ^~~~~~~~~~~~~~~~~

What is the reason for that?

2

Based on this AdaCore Release Notes — AdaCore Release Notes 24.0 documentation

That SPARK-specific aspect is only applicable to procedures definitions. Nothing mentions being able to apply it to an access-to-subprogram type.

3

From what I understand reading the User’s Guide 7.4. How to Write Subprogram Contracts — SPARK User's Guide 26.0w The aspect is always implicit and has to be marked for procedures where the loops do not have invariants.

5.2. Subprogram Contracts — SPARK User's Guide 26.0w gives a bit more info too.

4

Access to subprogram types and dispatching calls could hide recursive calls, so Always_Terminates on access to subprogram types is not allowed to ensure soundness in the termination analysis. Even if it was supported, it would probably be very restrictive.

I hit a similar problem a while back and my workaround was just to use a case statement to select from the set of possible subprogram targets. Not ideal, but it allowed for proving termination in my case.

1 Like