Verifica formale della correttezza mediante triple di Hoare
/* verificazione della proprietà di antisimmetria */
/* il primo elemento della coppia è <= del secondo ed il secondo
è <= del primo allora i due elementi della coppia ordinata
devono essere uguale perchè la proprietà antisimmetrica sia rispettata */
if(relazione_binaria[i].a <= relazione_binaria[i].b &&
relazione_binaria[i].b <= relazione_binaria[i].a)
{
if(relazione_binaria[i].a == relazione_binaria[i].b)
prop_antisimmetria = true;
else
prop_antisimmetria = false;
}
else
prop_antisimmetria = false;
Verifica della postcondizione inclusa nellÂÂÂ’if:
{
if(relazione_binaria[i].a == relazione_binaria[i].b)
prop_antisimmetria = true;
else
prop_antisimmetria = false;
}
Data una tripla di Hoare {Q} S {R}
Postcondizione R = prop_antisimmetria = true Or prop_antisimmetria = false
“if (beta) S1 else S2”
wp(S, R) = ((beta --> wp(S1, R)) or ((not beta) --> wp(S2, R)))
(relazione_binaria[i].a == relazione_binaria[i].b ->
(prop_antisimmetria)[prop_antisimmetria/true]) =
(relazione_binaria[i].a == relazione_binaria[i].b -> true) = vero
(relazione_binaria[i].a != relazione_binaria.b ->
(prop_antisimmetria)[prop_antisimmetria/false]) =
(relazione_binaria[i] != relazione_binaria[i].b -> false) = vero
vero and vero = vero
La postcondizione è vera
La precondizione è vera
