Questo sito utilizza cookies, anche di terze parti, per mostrare pubblicità e servizi in linea con il tuo account. Leggi l'informativa sui cookies.
Username: Password: oppure
C/C++ - come verificare con tripla di hoare
Forum - C/C++ - come verificare con tripla di hoare

Avatar
fulo305 (Normal User)
Newbie


Messaggi: 1
Iscritto: 13/09/2015

Segnala al moderatore
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

PM Quote
Avatar
Trusted (Normal User)
Newbie


Messaggi: 14
Iscritto: 06/09/2015

Segnala al moderatore
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++

  1. { x >= 0 && y > 0 } #Precondizione
  2.  
  3. q,r := 0,x;
  4.  
  5. while r >=  y do
  6.        q,r := q + 1, r - y
  7. endw
  8.  
  9. {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


Io oso tutto ciò che è degno di un uomo, chi osa di più non lo è.
PM Quote