C/C++ - come verificare con tripla di hoare

Forum - C/C++ - come verificare con tripla di hoare

fulo305 (Normal User)
Newbie

Messaggi: 1
Iscritto: 13/09/2015

Postato alle 14:02
Domenica, 13/09/2015

salve ragazzi,
sto facendo una relazione di un progetto e mi è richiesto di scegliere all’interno del programma una sequenza di almeno tre
istruzioni non di input/output la cui postcondizione non sia banalmente una tautologia e verificarne formalmente la correttezza mediante triple di Hoare.

avrei scelto queste righe di codice ma non capisco come devo fare per verificarle ho letto diverse dispense e post su internet mi potete aiutare

for(corr_p_1ciclo = insieme_p;
     ((corr_p_1ciclo != NULL) &&(strcmp(elem_ins, elem_ins2)!=0));
      corr_p_1ciclo = corr_p_1ciclo->succ_p, i++)

        {
            strcpy(elem_ins ,corr_p_1ciclo-> elem);
            esito_ass = 0;
        }

grazie mille a tutti

Trusted (Normal User)
Newbie

Messaggi: 14
Iscritto: 06/09/2015

Postato alle 10:17
Domenica, 20/09/2015

Ciao!
Allora in breve le triple di Hoare sono un modo per verificare il corretto funzionamento di un programma e prevenire errori. Vengono comunemente rappresentate da terne come {M} N {Z} dove N è un comando (o istruzione) ed M e Z sono dette Precondizione e Postcondizione

Questo è un esempio d'uso di una tripla di Hoare per verificare l'esecuzione del calcolo del quoziente.

Codice sorgente - presumibilmente C/C++

{ x >= 0 && y > 0 } #Precondizione
 
q,r := 0,x;
 
while r >=  y do
       q,r := q + 1, r - y
endw
 
{x = y * q + r  &&  0 <= r < y }#Postcondizione

Ora qui le asserzioni sono fatte ad hoc sarebbe meglio non operare guidati dagli errori.

Ora se sei arrivato qui (la sintesi in argomenti che amo non è da me. :love:

) per verificare le condizioni puoi scriverti
una funzione che fa il check delle condizioni e in caso positivo esegue il resto del codice altrimenti lo blocca

Spero di esserti utile :rofl:

Ultima modifica effettuata da Trusted il 20/09/2015 alle 10:22