โŒ About FreshRSS

Normal view

There are new articles available, click to refresh the page.
Before yesterdayNews from the Ada programming language world

Self dependency in Spark 2014

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 ?

โŒ
โŒ