Самостоятельность в Spark 2014

Question

Я пытаюсь написать зависимость потока процедуры в Ada и Spark 2014, и компилятор выдает мне среднее предупреждение, что

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

Вот мой файл .ads:

      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;

и в .adb:

      pragma SPARK_Mode (On);
package body TestDep is

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

end TestDep;

Я новичок в Ada и Spark, и я все еще изучаю это, но из документации AdaCore я видел, чтоDepends => (X =>+ null)должно указывать, что значение в конце процедуры зависит только от значенияXи ничего больше.

Почему компилятор выдает мне эти предупреждения? Я делаю что-то неправильно ?