--- layout: fc_discuss_archives title: Message 31 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,

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/20081110/555f8a2f/attachment.html