Commit 13e7f119 by MARCHE Claude

### jessie3: new examples to be proven

parent 5d150450
 /* run.config OPT: -journal-disable -jessie3 */ /* COST Verification Competition. vladimir@cost-ic0701.org Challenge 1: Maximum in an array Given: A non-empty integer array a. Verify that the index returned by the method max() given below points to an element maximal in the array. */ /*@ requires len > 0 && \valid(a+(0..(len-1))); @ ensures 0 <= \result < len && @ \forall integer i; 0 <= i < len ==> a[i] <= a[\result]; @*/ int max(int *a, int len) { int x = 0; int y = len-1; /*@ loop invariant 0 <= x <= y < len && @ \forall integer i; @ 0 <= i < x || y < i < len ==> @ a[i] <= \max(a[x],a[y]); @ loop variant y - x; @*/ while (x != y) { if (a[x] <= a[y]) x++; else y--; } return x; } /* Local Variables: compile-command: "frama-c -add-path ../.. -jessie3 array_max.c" End: */
 /* run.config OPT: -journal-disable -jessie3 */ /* selection sort */ /*@ predicate Swap{L1,L2}(int *a, integer i, integer j) = @ \at(a[i],L1) == \at(a[j],L2) && @ \at(a[j],L1) == \at(a[i],L2) && @ \forall integer k; k != i && k != j @ ==> \at(a[k],L1) == \at(a[k],L2); @*/ /*@ inductive Permut{L1,L2}(int *a, integer l, integer h) { @ case Permut_refl{L}: @ \forall int *a, integer l, h; Permut{L,L}(a, l, h) ; @ case Permut_sym{L1,L2}: @ \forall int *a, integer l, h; @ Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ; @ case Permut_trans{L1,L2,L3}: @ \forall int *a, integer l, h; @ Permut{L1,L2}(a, l, h) && Permut{L2,L3}(a, l, h) ==> @ Permut{L1,L3}(a, l, h) ; @ case Permut_swap{L1,L2}: @ \forall int *a, integer l, h, i, j; @ l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==> @ Permut{L1,L2}(a, l, h) ; @ } @*/ /*@ predicate Sorted{L}(int *a, integer l, integer h) = @ \forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ; @*/ /*@ requires \valid(t+i) && \valid(t+j); @ assigns t[i],t[j]; @ ensures Swap{Old,Here}(t,i,j); @*/ void swap(int t[], int i, int j) { int tmp = t[i]; t[i] = t[j]; t[j] = tmp; } /*@ requires \valid(t+(0..(n-1))); @ behavior sorted: @ ensures Sorted(t,0,n); @ behavior permutation: @ ensures Permut{Old,Here}(t,0,n-1); @*/ void min_sort(int t[], int n) { int i,j; int mi,mv; if (n <= 0) return; /*@ loop invariant 0 <= i < n; @ for sorted: @ loop invariant @ Sorted(t,0,i) && @ (\forall integer k1, k2 ; @ 0 <= k1 < i <= k2 < n ==> t[k1] <= t[k2]) ; @ for permutation: @ loop invariant Permut{Pre,Here}(t,0,n-1); @ loop variant n-i; @*/ for (i=0; i t[k] >= mv); @ for permutation: @ loop invariant @ Permut{Pre,Here}(t,0,n-1); @ loop variant n-j; @*/ for (j=i+1; j < n; j++) { if (t[j] < mv) { mi = j ; mv = t[j]; } } L: swap(t,i,mi); //@ assert Permut{L,Here}(t,0,n-1); } } /* Local Variables: compile-command: "frama-c -add-path ../.. -jessie3 selection_sort.c" End: */
 /* run.config OPT: -journal-disable -jessie3 */ typedef unsigned int size_t; void *malloc(size_t size); void *calloc(size_t nmemb, size_t size); typedef unsigned int uint; const uint DEFAULT = 0; typedef struct SparseArray { uint sz; uint n; int *val; uint *idx, *back; } *sparse_array; /*@ predicate is_elt{L}(sparse_array a, integer i) = @ 0 <= a->idx[i] < a->n @ && a->back[a->idx[i]] == i @ ; @*/ /*@ axiomatic Model { @ logic integer model{L}(sparse_array a,integer i); @ axiom model_in: \forall sparse_array a, integer i; @ is_elt(a,i) ==> model(a,i) == a->val[i]; @ axiom model_out: \forall sparse_array a, integer i; @ !is_elt(a,i) ==> model(a,i) == DEFAULT; @} @*/ /*@ predicate inv(sparse_array a) = @ \valid(a) && @ 0 <= a->n <= a-> sz && @ \valid(a->val+(0..a->sz-1)) && @ \valid(a->idx+(0..a->sz-1)) && @ \valid(a->back+(0..a->sz-1)) && @ \forall integer i; 0 <= i < a->n ==> @ 0 <= a->back[i] < a->sz && a->idx[a->back[i]] == i; @*/ /*@ requires sz >= 0; @ assigns \nothing; @ allocates \result; @ ensures inv(\result); @ ensures \result->sz == sz; @ ensures \forall integer i; model(\result,i) == DEFAULT; @*/ sparse_array create(uint sz) { sparse_array a = (sparse_array)malloc(sizeof(struct SparseArray)); a->val = (int*)calloc(sz,sizeof(int)); a->idx = (uint*)calloc(sz,sizeof(uint)); a->back = (uint*)calloc(sz,sizeof(uint)); a->n = 0; a->sz = sz; return a; } /*@ requires \valid(a); @ requires inv(a); @ requires i <= a->sz - 1; @ assigns \nothing; @ ensures \result == model(a,i); @*/ int get(sparse_array a, uint i) { // note: 0 <= a->idx[i] holds because of type uint //@ assert 0 <= a->idx[i]; if (a->idx[i] < a->n && a->back[a->idx[i]] == i) return a->val[i]; else return 0; } /*@ requires \valid(a); @ requires inv(a); @ requires i <= a->sz - 1; @ assigns a->val[i],a->idx[..],a->back[..], a->n; @ ensures inv(a); @ ensures model(a,i) == v; @ ensures \forall integer j; j != i ==> @ model(a,j) == \old(model(a,j)); @*/ void set(sparse_array a, uint i, int v) { a->val[i] = v; if (!(a->idx[i] < a->n && a-> back[a->idx[i]] == i)) { // the following assertion is hard to prove //@ assert a->n < a->sz; a->idx[i] = a->n; a->back[a->n] = i; a->n++; } } int main() { sparse_array a = create(10), b = create(20); int x,y; x = get(a,5); y = get(b,7); //@ assert x == 0 && y == 0; set(a,5,1); set(b,7,2); x = get(a,5); y = get(b,7); //@ assert x == 1 && y == 2; x = get(a,0); y = get(b,0); //@ assert x == 0 && y == 0; return 0; } /* Local Variables: compile-command: "frama-c -add-path ../.. -jessie3 sparse_array.c" End: */
 /* run.config OPT: -journal-disable -jessie3 */ /* Area of a triangle, a formale revisit * http://hal.inria.fr/hal-00790071 */ /*@ requires 0 <= x; @ ensures \result==\round_double(\NearestEven,\sqrt(x)); @*/ double sqrt(double x); /*@ logic real S(real a, real b, real c) = @ \let s = (a+b+c)/2; @ \sqrt(s*(s-a)*(s-b)*(s-c)); @ */ /*@ requires 0 <= c <= b <= a && a <= b + c && a <= 0x1p255; @ ensures 0x1p-513 < \result @ ==> \abs(\result-S(a,b,c)) <= (53./8*0x1p-53 + 29*0x1p-106)*S(a,b,c); @ */ double triangle (double a,double b, double c) { return (0x1p-2*sqrt((a+(b+c))*(a+(b-c))*(c+(a-b))*(c-(a-b)))); } /* Local Variables: compile-command: "frama-c -add-path ../.. -jessie3 triangle.c" End: */
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!