[Spark2014-discuss] Attribute for initial value of a parameter? validity of an array as parameter?

Hugues Jérôme hugues.jerome at gmail.com
Wed Jul 9 14:05:36 CEST 2014


Hi,

in my attempt to complete ACSL-by-Example in SPARK2014 (my daily brain exercise currently), 
I stumbled into two minor issues

- how can we perform assessments (assert, loop_invariant, etc) on initial value of a parameter?
Let me explain: I considered this function:

  --  6.3 The swap_ranges Algorithm
  --
  -- The swap_ranges algorithm in the C++ STL exchanges the contents
  --  of two expressed ranges element-wise.

  procedure Swap_Range (X : in out T_Arr; Y : in out T_Arr)
    with
    Pre => (X'First = Y'First and X'Last = Y'Last
           and X'Last > X'First and Y'Last > Y'First),
    Post => ((for all J in X'Range => X (J) = Y'Old (J)) and then
               (for all J in X'Range => X'Old (J) = Y (J)));

and I came with this solution:

  procedure Swap_Range (X : in out T_Arr; Y : in out T_Arr) is
  begin
     Inner : for J in X'Range loop
        Swap (X (J), Y (J));
        pragma loop_invariant
          (for all K in X'first .. J => X'Loop_Entry (Inner) (K) = Y (K));
        pragma loop_invariant
          (for all K in Y'first .. J => Y'Loop_Entry (Inner) (K) = X (K));
        pragma loop_invariant
          (for all K in J .. X'Last => (if K <= X'Last and K > J then X (K) = x'Loop_entry (inner) (K)));
        pragma loop_invariant
          (for all K in J .. Y'Last => (if K <= Y'Last and K > J then Y (K) = Y'Loop_entry (inner) (K)));
     end loop Inner;
  end Swap_Range;

*but*, in ACSL they use the following invariant (see p 74 of the PDF)

loop invariant IsEqual{Pre,Here}(a, i, b);

the subtle difference I note is that the label Pre denotes the initial value at the *beginning of the function*
Here, I used Loop_entry, which is the value at before entering the loop. This is equivalent for this simple function. 
But I’m curious: did you consider an attribute for supporting the Pre label ? ‘Old seems not usable in this context

- when I have function with arrays as parameters, I see errors when considering something like X (X’First)
After some self-interrogation, I came to the conclusion X’First may be invalid considering an empty array (e.g. X’Last < X’First)
and force pre-conditions as 

  procedure Swap_Range (X : in out T_Arr; Y : in out T_Arr)
    with
    Pre => (X'First = Y'First and X'Last = Y'Last
           and X'Last > X'First and Y'Last > Y'First),

to lift this warning. Is there a more spark-compliant way of doing this ? Basically, the pre-condition would be “this array is not ill-formatted”
I can of course define my own predicate to support this

Finally, it seems I cannot do X’Range = Y’Range, is there a better way than (X'First = Y'First and X'Last = Y’Last ?

Thanks!


More information about the Spark2014-discuss mailing list