[Spark2014-discuss] Foo'Result'First strange behavior

Hugues Jérôme hugues.jerome at gmail.com
Tue Jul 22 13:56:23 CEST 2014


I’m playing again with SPARK2014. This time, the problem I propose to the community is the following

Let us suppose:

     function Reverse_Copy (X : T_Arr) return T_Arr with
       Pre => (X'Last > X'First),
       Post => (Reverse_Copy'Result'Last = X'Last and
                Reverse_Copy'Result'First = X'First and
                (for all K in Reverse_Copy'Result'Range =>
                  Reverse_Copy'Result (K) = X (X'Last - K + X'First)));

with the following implementation

  function Reverse_Copy (X : T_Arr) return T_Arr is
     Result : T_Arr (X'First .. X'Last);
     for J in Result'Range loop
        Result (J) := X (X'Last - J + X'First);
        pragma Loop_Invariant
          (for all K in Result'First .. J =>
             Result (K) = X (X'Last - K + X'First));
     end loop;

     pragma Assert (Result'Last = X'Last);  — line 61
     pragma Assert (Result'First = X'First);  —  line 62
--      pragma Assert (for all K in Result'Range =>
--                     Result (K) = X (X'Last - K + X'First));

     return Result;
  end Reverse_Copy;

The “strange” behavior I see is the following:
- the two assertions are proved

chap6.adb:61:7: info: assertion proved()
chap6.adb:62:7: info: assertion proved()

- but not the postcondition

chap6.ads:61:18: warning: postcondition might fail, requires Reverse_Copy'Result'Last = X'last()

AFAICT, the postcondition and the assertion refers to the same entity. Is it a known limitation in the toolset?
Or an obvious error in my own code? I’m puzzled to say the least, and I moved to another example in the mean time

Full code for the interested reader is in chap6.ads in https://github.com/yoogx/spark_examples/tree/master/spark-by-example


More information about the Spark2014-discuss mailing list