C/C++ - Tripla di Hoare su un codice c

Salve ragazzi, pur avendo fatto alcune ricerche su internet non riesco ancora a capire bene la tripla di Hoare. Ho capito che serve per formalizzare la correttezza di un programma, solo che il prof ci ha assegnato, nel progetto, questa consegna:

Verifica del programma: scegliere una sequenza di almeno tre istruzioni di senso compiuto all'interno del programma e verificarne formalmente la correttezza tramite triple di Hoare

e mi trovo un po sperduto. Qualcuno può darmi qualche dritta?

PS ho postato qui perchè comunque il codice sviluppato è in c, ma nel caso avessi sbagliato ditemelo!

Beh, hai letto qui? it.wikipedia.org/wiki/…

Cosa non riesci a capire?

Sì, sì ho letto, come ho letto (e cercato di capire) le dispense del prof e varie pagine cercate per la rete, ma mi risulta ostico capire come applicarlo alle istruzioni di un programma.
Io avevo in mente di verificare la correttezza delle istruzioni if-else, tipo

    if (contr > 0)
        printf("\nLe formule non sono equivalenti.\n");
    else
        printf("\nle formule sono equivalenti.\n");

ma ho molti dubbi: 1) come faccio in pratica, a mettere in atto le regole delle triple di hoare su queste istruzioni, 2) l'istruzione che ho scelto può essere formalmente verificata (dopotutto il valore di contr io non lo conosco solo da queste istruzioni).

Capisco che sembrano domande di uno che non ha completamente studiato, ma la verità è che ho capito molto poco, molto poco.

Se contr non e' conosciuto, devi formulare due casi:

Caso #1 contr > 0
Caso #2 contr <= 0

E fare la verifica per entrambi i casi.

Quindi teoricamente il blocco if-else è corretto, perchè:

la post condizione è (printf(equivalenti) V printf(non equivalenti))

quindi

(contr > 0) -> (printf(equivalenti) V printf(non equivalenti)) = Vero
(contr <= 0) -> (printf(equivalenti) V printf(non equivalenti)) =Vero
Vero && Vero = Vero

è più o meno così il ragionamento?

{P} S {Q}

P = contr > 0 V contr <= 0
S = contr > 0 --> print('Non equivalenti'), contr <= 0 --> print('Equivalenti')
Q = print('Non equivalenti') V print('Equivalenti')

Personalmente questo esempio ha veramente poco senso perche' non c'e' nulla di utile da dimostrare, forse dovresti scegliere una parte del programma che potrebbe giovare da una verifica formale (che ne so, un calcolo matematico, oppure che il programma non andra' mai in loop infinito). Alcune slides interessanti: cs.cmu.edu/~aldrich/courses/413/slides/…