C/C++ - Verifica formale tramite triple Hoare

Ciao a tutti, mi viene chiesto di verificare formalmente la correttezza di una porzione di codice tramite triple di Hoare. La porzione di codice che ho scelto è una funzione per la verificazione della proprietà di antisimmetria. Quindi 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. Questo è quello che ho scritto, può andare bene? Grazie mille a chiunque possa aiutarmi!

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