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

while ( (var_indice1 < VAR1) && (res == OK) )
{

while ( (var_indice2 < VAR2) && (res== OK) )
{ // traitement
}
}
IE : Il Existe
QS : Quel que soit
APP : Appartient
&& : Et
v : Ou
IMP : Implique
VAR1 et VAR2 sont des constantes

QS indice1, indice2 APP int.
indice2 >= 0 && indice2 < VAR2 && indice1 >= 0 && indice1 < VAR1 IMP
TAB[VAR2*indice2 +indice1] = OK
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".

C'est plus une question de mathématiques que d'informatique, mais peut-être que quelqu'un ici sait ?

Merci