/* @ axiomatic CountTab{ logic integer countTab{L}(int *t, integer n, int v) reads t[0 .. n-1]; axiom CountEmptyTab: Dans un tableau vide, il y a zéro éléments. axiom MatchElem: Si l’élément k-1 est v, alors, entre 0 et k, il y a un v de plus qu’entre 0 et k-1. axiom MissElem: Si l’élément k-1 n’est pas v, alors, entre 0 et k, il y a autant de v qu’entre 0 et k-1. } */ /* à compléter @ ensures \result == countTab(t,n,val); */ int countTab(int *t, int n, int val){ if(n<=0) return 0; else{ int res = 0; /* invariants et variant. */ for(int i = 0; i