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

[Frama-c-discuss] Composition of COMPLEX Contracts



Hi, and thank you for the help.

I added an assigns clause and a loop assigns but the post-condition cannot be proven (Hydrogen). Is there something else missing or is it due to the Hydrogen.

Christoph
  ----- Original Message ----- 
  From: Yannick Moy 
  To: Christoph Weber 
  Cc: frama-c-discuss@lists.gforge.inria.fr 
  Sent: Monday, November 10, 2008 11:49 PM
  Subject: Re: [Frama-c-discuss] Composition of COMPLEX Contracts


  Hi,

  You need to express that [copy] may modify the content of the array pointed-to by dest, which can be as simple as

  //@ assigns dest[..];

  or with more precision

  //@ assigns dest[0..last-first];


  HTH,
  Yannick



  On Mon, Nov 10, 2008 at 1:58 PM, Christoph Weber <Christoph.Weber@first.fraunhofer.de> wrote:

    Hello again,

    this time I am doing some exercises with Hydrogen.

    I am using the copy algorithm to implement a rotate function:
    It copies the values of the elements in the range [first,last) to the range positions 
    beginning at result, but rotating the order of the elements in such a way that the 
    element pointed by middle becomes the first element in the resulting range.

    rotate_copy===========================

    #include "copy.h"
    #include "predicates.h" 
    /*@
    requires last > middle >= first;
    requires \valid_range (first, 0, last-first-1);
    requires \valid_range (dest, 0, last-first-1);
    requires disjoint_arrays(first, dest, last-first);


    ensures \forall integer i; 0 <= i < middle-first ==> dest[i] == middle[i];
    ensures \forall integer i; middle-first <= i < last-middle ==> dest[i] == first[i];
    */
    int* rotate_copy (int* first, int* middle, int* last, int* dest ) 
    {
    dest = copy (middle, last, dest);
    return copy (first, middle, dest);
    }
    =========================================
    copy.h====================================
    /*@
    requires last > first;
    requires disjoint_arrays(first, dest, last-first);
    requires \valid_range (first, 0, last-first-1);
    requires \valid_range (dest, 0, last-first-1);
    assigns \nothing;
    ensures \forall integer i; 0 <= i < last-first ==> dest[i] == first[i];
    */
    int* copy (int* first, int* last, int* dest); 
    =========================================
    copy.c====================================
    #include "copy.h" 
    int* copy (int* first, int* last, int* dest) 
    {
    int* it1 = first;
    int* it2 = dest;
    /*@
    loop invariant first <= it1 <= last;
    loop invariant it2 - dest == it1 - first;
    loop invariant dest <= it2 <= dest + (last-first); 
    loop invariant \forall integer k; 0 <= k < it1-first ==> first[k] == dest[k]; 
    */
    while (it1 != last)
    {
    *it2++ = *it1++;
    }
    return it2;
    }

    The Problems are as followed:

    The assigns clause in copy.h is nonesense but "assigns dest " will work even less. ()

    with assigns \nothing i get copy.c proven but rotate_copy fails with preconditions.

    My qeuestion is: What has to be added to get it through.



    Cheers 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/20081111/af6386c6/attachment.html