Please note that this website is still in development phase and might change even in V1
All .pdf subjects available in this repository are the exclusive property of the University of Bourgogne Franche Comte. Any reproduction, use outside the academic framework of the university, or without permission, is prohibited and may be considered as an infringement.
On commence par réécrire le triplet
On utilise la règle sequence pour remplacer la postcondition {x=-y) par x=-(y-1) soit x=-y+1
En utilisant la règle de précondition x=-y on obtient un nouveau triplet
L’implication x = -y ∧ x # n ⇒ x + 1 = -y + 1 résulte de A ∧ B ⇒ A et de x = y ⇒ x + 1 = -y + 1
x=-y ∧ x#n => x+1=-y+1
vu qu'on obtient x+1=-y+1 on va faire un assignment dans la précondition pour rempplacer x=-y par x+1=-y+1
{x+1=-y+1} x:=x+1 {x=-y+1}
On commence par réécrire le triplet
{z=0} while z=z do z:=z+1 od {z=2}
Nous allons simplifier le triplet avec la règle conséquence
la conséquence de z=0 est z>=0.
Pour la postcondition vu que z=2 on peut en déduire que z sera encore >=0
Pour simplifier ce qui est entre la précondition et la postcondition on peut utiliser la règle pour l'instruction itérative (while)
la précondition devient {z=z ∧ z>=0}
mais en utilisant la régle de la précondition vu que z=z zt que l'instruction donne z=z+1 on peut avoir
{z+1>=0} z:=z+1{z>=0}
Pour la postcondition, vue que c'est une boucle infinie mettre des trucs faux => osef donc c'est vrai. donc on peut mettre un truc vrai comme z>=0
Cela reprend le principe de l'implication absurde comme "lorsque les poules auront des dents, truc qui nous semble impossible" est parfaitement vraie.
Pour rappel a=bq+r.
Pour tous les entiers naturels a et b non nuls. La précondition est donc {a>=0 ∧ b>0}
Pour les instructions, on recopie le programme
Pour la postcondition on met a=bq+r et que le reste est compris entre 0 et le diviseur. Soit {a=bq+r ∧ 0<=r < b }
On recopie le triplet mais on peut mettre les éléments d'avant le while dans la précondition avec la règle assigment
On peut également modifier la postcondition en précisant si a b q et r sont supérieur à 0 avec cette même règle assigment
Pour la 2 ce n'est que le résultat de l'assignment il n'y a plus d'instruction avant le while car on les a rentré dans la précondition
pour la 3 avec la règle d'assignment on utilise q:=0 pour remplacer q par 0 dans la précondition et dans la postcondition. On utilise égalmeent le fait que dnas la 2 on ait r:=a pour remplacer tout les r par des a
pour la 4 la règle séquence nous pemret d'utiliser le programme en mettant a:=a dans la précondition en reprenant r:=a
On veut maintenant ce débarasser de a=a dnas la précondition et de q:=0
On montre que a>=0 ∧ b>0 implique déjà q:=0 et r:=a
Avec la règle séquence on confirme nôtre justification
Avec la règle de la précondition vu que a>=0 ∧ b>0 implique q:=0 et r:=a o nobtient le triplet souhaité
L'invariant de boucle est ce qui ne change jamais avant, pendnat et après la boucle. a=bq+r est toujours vraie et le reste est toujours supérieure ou égale à 0.
void inversion (int tab[], int n, int out[]) { int i = 0; while (i < n) { // Q1: 0.5 pt out[i] = tab[n-1-i]; // Q1: 0.5 pt i = i+1; // Q1: 0.5 pt } }
Pour donner en syntaxe micro-C une précondition pour que le tableau out ait une taille suffisante pour contenir les éléments du tableau tab dans l’ordre inverse.
Il est donc requis que la longueur du tableau out soit supérieure ou égale à n.
//* requires length(out) >=n;
Donner en syntaxe micro-C une postcondition qui exprime que le tableau out contient les éléments du tableau tab dans l’ordre inverse
Il faut donc s'assurer que pour tout élément du tableau out correspond les éléments d'indice de tab dans l'ordre inverse.
ensures forall i. 0 <= i < n -> out[i] == tab[n-1-i];
l'invariant est assez compliqué à définir
on peut déjà mettre que 0<=i<=n car i=0 et while (i inf n)
Ce qu'il ne faut pas oublier c'est que tous les éléments du tableau tab soit inverser dans le bon ordre dans out
On veut vérifier qu'à chaque étape les i premiers termes du tableau sont bons, donc on check le terme j pour j allant de 0 à i.
Le variant de boucle est n-i car while ( i inférieur à n)
Par définition, la racine carrée entière par excès de n est le plus petit entier naturel dont le carré est supérieur ou égal à n.
Ce programme doit être composé d’une initialisation, d’une boucle while et d’une instruction (s := s - 1) de décrémentation.
Avec ces éléments, on a donc while et s:=s-1. On doit donc décrémenter une valeur
Vu que la racine carrée entière par excès de n est le plus petit entier naturel dont le carré est supérieur ou égal à nn on va utiliser une variable n.
s,n while s:=s-1
par dérémentation à partir de la valeur initiale n.
Il faut donc s:=n while s:=s-1
Il faut comparer s avec n pour avoir : Par définition, la racine carrée entière par excès de n est le plus petit entier naturel dont le carré est supérieur ou égal à n
On a donc s:=n;while(s-1)^2>=n do s:=s-1 od
La précondition la plus générale est {n>0} car Soit n un entier naturel (n ≥ 0 en tant qu’entier relatif).
la postcondition devant caractériser une valeur unique pour s, quel que soit l'entier strictement positif n.
On peut commencer par remprendre notre triplet de hoare et constaté que avec le while on a (s-1)^2< n .
vu que dans la boucle on décrément s de 1 cela signifie que s^2 est plus grand que n et (s-1)^2.
On a donc {n > 0} s := n; while (s - 1)2 ≥ n do s := s - 1 od {(s - 1)2 < n ≤ s2}
L'invariant de la boucle étant ce qui ne varie jamais on peut reprendre la postcondition. Il faut donc qu'il soit suffisant pour démontrer la validité de ce triplet de Hoare.
en micro C la précondition ce formule par requires c'est ce qui est requis avant de passer aux instructions.
La postcondition en micro C se formule avec ensures pour s'assurer que tous c'est bien passé et que le programme a bien effectué ce qui était attendu.
On met donc avoir ouvert l'accolade ouvrante de la fonction /* requires ...; ensures ...; */ */
On a donc /*@requires 0< n; ensures (result-1)*(result-1) < n <= result*result; */
L'invariant de boucle est ce qui ne varie pas dans le programme après avoir effectuer une boucle
le variant de boucle c'est ce qui varie après la boucle.
On met donc après le while ou le for à l'intérieur de la boucle /*@ invariant ... ; variant ...; */
On a donc /*@ invariant n <= s*s && 0 <= s; vraient s; */
predicate eq(int a[], int b[]) = ...;
Pour que les tableaux soient égaux il faut que la taille des deux tableaux soient égaux et que pour chaque éléments i du tableau on ait les mêmes valeur entre les 2 tableaux
On a donc /*@ predicate eq(int a[], int b[]) = lenth(a) == length(b) && forall i.0 <= i < legth(a) -> a[i] == b[i]; */
on a une croix verte puis un point d'interrogation jaune.
cet affichage signifie que le premier lemme a été démontré et uqe le second lemme n'a pas été démontré. Le prouveur étant supposé correct, ceci signnifie que le premeir lemme est vrai. Le prouveur n'étant pas complet, on ne peut rien déduire de l'absence de preuve pour le second lemme.