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

Yannick Moy moy at adacore.com
Wed Jul 9 21:22:20 CEST 2014


Hi Jérôme.,

-- Hugues Jérôme (2014-07-09)
> 
> Hi,
> 
> in my attempt to complete ACSL-by-Example in SPARK2014 (my daily brain exercise currently), 

I agree, it's much better than crosswords or Dr Kawashima. :)

> I stumbled into two minor issues
> 
> - how can we perform assessments (assert, loop_invariant, etc) on initial value of a parameter?

We have already noted as a possible future enhancement to create an attribute Subprogram_Entry to denote the value of an object at subprogram entry, like we have currently Loop_Entry, but its value does not seem very high right now. First, in most cases you can use Loop_Entry instead (like in your example). Secondly, it will be possible in the next release to introduce a ghost variable to hold the copy of an object anywhere, in particular at subprogram entry.

> 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;

note that, since you have no nested loops, you can safely use X'Loop_Entry here instead of X'Loop_entry (Inner), you won't fall in the bug of SPARK GPL 2014.

> *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

Indeed, attribute Old is defined by Ada, so we cannot expand its definition. It should only occur in postconditions (and contract_cases, which are like postconditions).

> - 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

You can use X'Length > 0 and Y'Length > 0.

> 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 ?


You could also make this procedure work for ranges of the same length that are not exactly the same.
If you want to express that they range over the same indexes, there is no better way that what you wrote, but you can factor this out in an expression function:

  function Same_Range (X, Y : T_Arr) return Boolean is (X'First = Y'First and X'Last = Y’Last);

Hope that helps.
--
Yannick Moy, Senior Software Engineer, AdaCore







More information about the Spark2014-discuss mailing list