Bonjour,
je fais de la preuve formelle de programme, preuve qui se fait (en partie) à partir de formules logiques.
Vu que c'est le début, je reprend un programme déjà prouvé, et je tente de refaire la preuve à partir des hypothèses de départ.
J'ai une formule qui me gêne.
Cette formule traduit des conditions de boucle
IE : Il Existewhile ( (var_indice1 < VAR1) && (res == OK) )
{
while ( (var_indice2 < VAR2) && (res== OK) )
{ // traitement
}
}
QS : Quel que soit
APP : Appartient
&& : Et
v : Ou
IMP : Implique
VAR1 et VAR2 sont des constantes
Ce que j'ai oublié, c'est pourquoi je ne peux pas utiliser mes variables, et que je suis obligé de passer par un "Quel que soit".QS indice1, indice2 APP int.
indice2 >= 0 && indice2 < VAR2 && indice1 >= 0 && indice1 < VAR1 IMP
TAB[VAR2*indice2 +indice1] = OK
C'est plus une question de mathématiques que d'informatique, mais peut-être que quelqu'un ici sait ?
Merci![]()
Partager