--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE yet another specification example :)



Hi,

Here is a correct loop invariant for your function:

    /*@
     loop invariant a <= first <= last;
     loop invariant result - b == first - a;
     loop invariant b <= result <= b+length;
     loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == b[k];
    */

There were two problems with yours:
1) it was not strong enough to be inductive, because you did not relate the
value of result and first during looping, this is the part [result - b ==
first - a]
2) there was an error in the last line, you meant to use the unmodified
ghost versions of your pointers!

With the Hydrogen version, I do not succeed to prove the postcondition, but
with Helium it goes through with Z3.

HTH,
Yannick

On Fri, Oct 17, 2008 at 8:54 AM, Christoph Weber <
Christoph.Weber@first.fraunhofer.de> wrote:

>  Hello again,
>
> I'm trying to explore a new example combining array_cpy(int* a, int n, int*
> b); and fill_int_array(int* first, int* last, int value).
>
> This one is called copy_int_array (int* first, int* last, int* result).
>
>  DESCRIPTION:
>   Copies the elements in the range [first,last) into a range beginning at
> result.
>   Returns an iterator to the last element in the destination range.
>
>  Parameters:
>   first, last:
>    Pointers to the initial and final positions of the searched sequence.
> The range
>    used is [first,last), which contains all the elements between first and
> last,
>    including the element pointed by first but not the element pointed by
> last.
>   result
>    Pointer to the initial position in the destination sequence. This shall
>    not point to any element in the range [first,last).
>   Return value:
>    A pointer to the last element of the destination sequence where elements
>
>    have been copied.
>    CODE:
>
> /*@ predicate disjoint_arrays(int* a, int* b, integer i) =
>      \forall integer k1, k2;
>         0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2;
> */
> /*@
>  requires last > first;
>  requires disjoint_arrays(first, result, last-first);
>
>  requires \valid_range  (first, 0, last-first-1);
>  requires \valid_range  (result, 0, last-first-1);
>  ensures  \forall integer i; 0 <= i < last-first ==> result[i] ==
> first[i];
> */
>
> int* copy_int_array (int* first, int* last, int* result)
> {
>  //@ ghost int* a = first;
>  //@ ghost int* b = result;
>  //@ ghost int length = last-first;
>
>     /*@
>      loop invariant a <= first <= last;
>      loop invariant b <= result <= b+length;
>      loop invariant \forall integer k; 0 <= k < first-a ==> result[k] ==
> first[k];
>     */
>   while (first!=last) *result++ = *first++;
>   return result;
> }
>
> Up to this moment Jessie is unable to solve it entirely.
>
> Am I missing something or is it due to my Hydrogen version.
>
> Greets
>
> Christoph
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>


-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/75aab429/attachment.htm