--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about partition.c




On 01/29/2015 07:03 PM, Marko Sch?tz Schmuck wrote:
> /*@ requires \valid(t)
>      && \valid(t+i) && \valid(t+j);
>    @*/

Why adding \valid(t) here ???

> void swap(int t[], int i, int j) {
>    int tmp = t[i];
>    t[i] = t[j];
>    t[j] = tmp;
> }
> /*@ requires 0 <= p <= r && \valid_range(A,p,r);
>    @*/
> int partition (int A[], int p, int r)
> {
>    int x = A[r];
>    int tmp, j, i = p-1;
>    /*@ loop invariant p <= j <= r
>                       && p-1 <= i < j
> 		     && \valid(A+j)
> 		     && \valid(A+i+1);

These last two invariants cannot be what you want ...

>      @ loop variant (r-j);
> there are 3 POs from the invariant that are not discharged. For
> example:
>
 > [...]

> Prove: (valid_rw Malloc_0 (shift A_0 x_1) 1).
> Prover Alt-Ergo returns Unknown (Qed:3ms) (1s)
>
> I fail to see why this PO is not automatically discharged. Also, how
> are the _0, _1, etc suffixes supposed to be read?

I guess that when calling swap(A,i,j), there is no way to prove the 
extra pre-condition \valid(t) you added.

Be careful with your annotations...

- Claude


> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |