[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