Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] YASE yet another specification example :)
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 17 10:38:16 2008
  • In-reply-to: <C91C76CE49FD41ACB52110216AA18A2D@AHARDPLACE>
  • References: <C91C76CE49FD41ACB52110216AA18A2D@AHARDPLACE>
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