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++ - Tripla di Hoare su un codice c
Forum - C/C++ - Tripla di Hoare su un codice c

Avatar
Kron_Os (Normal User)
Newbie


Messaggi: 8
Iscritto: 17/12/2013

Segnala al moderatore
Postato alle 13:20
Lunedì, 06/01/2014
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!


"tu che mi leggi sei sicuro di intendere la mia lingua?"
PM Quote
Avatar
pierotofy (Admin)
Guru^2


Messaggi: 6112
Iscritto: 04/12/2003

Segnala al moderatore
Postato alle 3:04
Martedì, 07/01/2014
Beh, hai letto qui? http://it.wikipedia.org/wiki/Logica_di_Hoare

Cosa non riesci a capire?


Seguimi su Twitter: http://www.twitter.com/pierotofy

Fai quello che ti piace, e fallo bene.
PM Quote
Avatar
Kron_Os (Normal User)
Newbie


Messaggi: 8
Iscritto: 17/12/2013

Segnala al moderatore
Postato alle 22:54
Martedì, 07/01/2014
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

Codice sorgente - presumibilmente C/C++

  1. if (contr > 0)
  2.         printf("\nLe formule non sono equivalenti.\n");
  3.     else
  4.         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.


"tu che mi leggi sei sicuro di intendere la mia lingua?"
PM Quote
Avatar
pierotofy (Admin)
Guru^2


Messaggi: 6112
Iscritto: 04/12/2003

Segnala al moderatore
Postato alle 17:38
Mercoledì, 08/01/2014
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.


Seguimi su Twitter: http://www.twitter.com/pierotofy

Fai quello che ti piace, e fallo bene.
PM Quote
Avatar
Kron_Os (Normal User)
Newbie


Messaggi: 8
Iscritto: 17/12/2013

Segnala al moderatore
Postato alle 19:40
Mercoledì, 08/01/2014
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?


"tu che mi leggi sei sicuro di intendere la mia lingua?"
PM Quote
Avatar
pierotofy (Admin)
Guru^2


Messaggi: 6112
Iscritto: 04/12/2003

Segnala al moderatore
Postato alle 22:47
Mercoledì, 08/01/2014
{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: http://www.cs.cmu.edu/~aldrich/courses/413/slides/24-hoare ...


Seguimi su Twitter: http://www.twitter.com/pierotofy

Fai quello che ti piace, e fallo bene.
PM Quote