0

I'm trying to write the flow dependency of a procedure in Ada and Spark 2014 and the compiler give me a medium warning that

medium: missing dependency "null => MyBool"
medium: incorrect dependency "MyBool => MyBool"

Here is my .ads file:

SPARK_Mode (On);
package TestDep is

  pragma Elaborate_Body;

  MyBool: Boolean := False;

  procedure ToFalse with
    Global => (In_Out => MyBool),
    Depends => (MyBool =>+ null),
    Pre => (MyBool = True),
    Post => (MyBool = False);

end TestDep;

and in the .adb:

pragma SPARK_Mode (On);
package body TestDep is

  procedure ToFalse is
  begin
    MyBool := False;
  end ToFalse;

end TestDep;

I'm new to Ada and Spark and I'm still learning it, but from the AdaCore documentation I've saw that Depends => (X =>+ null) should indicate that the value of X at the end of the procedure only depends on the value of X and nothing else.

Why does the compiler give me those warning ? Am I doing something wrong ?

Architek
  • 53
  • 5
  • 2
    `MyBool` is set to `False`, and thus does not depend on the initial value of `MyBool`. The `Global` should be just `Output`, not `In_Out` – egilhh Sep 26 '22 at 16:49
  • Yes, MyBool must be with `Global => (Output => MyBool)`. And then `Depends => (X =>+ null)` must be `Depends => (X => null)`. If you need more information, I can write an answer to this question. But I suppose, with these two comments it is clear. – habrewning May 07 '23 at 08:07

0 Answers0