/*@ axiomatic counting { logic integer count(int *a, integer debut, integer fin, int val) reads a[debut], a[fin-1]; axiom Count0: \forall int *a, val, integer debut; count(a, debut, debut, val) ==0; axiom Count1: \forall int *a, val, integer debut; (a[debut] == val ==> count(a, debut, debut +1, val) == 1) && (a[debut] != val ==> count(a, debut, debut +1, val) == 0); axiom Count2: \forall int *a, val, integer debut, k, fin; debut <= k <= fin ==> count(a, debut, fin, val) == count(a, debut, k, val) + count(a, k, fin, val); } lemma countLemma: \forall int *a, val, integer i; 0 <= i ==> count(a, 0, i+1, val) == count(a, 0, i, val) + count(a, i, i+1, val); */ /*@ ensures \forall int *a, val, integer i; 0 <= i ==> count(a, 0, i+1, val) == count(a, 0, i, val) + count(a, i, i+1, val); */ void dummy(void){ } /*@ requires n>= 0 && \valid_range(a, 0, n-1); assigns \nothing; ensures \result == count(a, 0, n, val); */ int count(int *a, int n, int val){ int cnt=0; int i; /*@ loop invariant 0 <= i <= n; loop invariant 0 <= cnt <= i; loop invariant cnt == count(a, 0, i, val); loop assigns i, cnt; loop variant n-i; */ for (i=0; i