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++ - Verifica formale tramite triple Hoare
Forum - C/C++ - Verifica formale tramite triple Hoare

Avatar
julver (Normal User)
Newbie


Messaggi: 1
Iscritto: 23/01/2015

Segnala al moderatore
Postato alle 13:41
Martedý, 27/01/2015
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!

Codice sorgente - presumibilmente Python

  1. Verifica formale della correttezza mediante triple di Hoare
  2.  
  3. /* verificazione della proprietÓ di antisimmetria */
  4.         /* il primo elemento della coppia Ŕ <= del secondo ed il secondo
  5.         Ŕ <= del primo allora i due elementi della coppia ordinata
  6.         devono essere uguale perchŔ la proprietÓ antisimmetrica sia rispettata */
  7.         if(relazione_binaria[i].a <= relazione_binaria[i].b &&
  8.         relazione_binaria[i].b <= relazione_binaria[i].a)
  9.         {
  10.         if(relazione_binaria[i].a == relazione_binaria[i].b)
  11.         prop_antisimmetria = true;
  12.         else
  13.         prop_antisimmetria = false;
  14.         }
  15.         else
  16.         prop_antisimmetria = false;
  17.  
  18.  
  19. Verifica della postcondizione inclusa nell┬┬┬ĺif:
  20.  
  21.            {
  22.         if(relazione_binaria[i].a == relazione_binaria[i].b)
  23.         prop_antisimmetria = true;
  24.         else
  25.         prop_antisimmetria = false;
  26.         }
  27.  
  28. Data una tripla di Hoare {Q} S {R}
  29.  
  30. Postcondizione R = prop_antisimmetria = true Or prop_antisimmetria = false
  31.  
  32. ôif (beta) S1 else S2ö
  33. wp(S, R) = ((beta --> wp(S1, R)) or ((not beta) --> wp(S2, R)))
  34. (relazione_binaria[i].a == relazione_binaria[i].b ->
  35. (prop_antisimmetria)[prop_antisimmetria/true]) =
  36. (relazione_binaria[i].a == relazione_binaria[i].b -> true) = vero
  37. (relazione_binaria[i].a != relazione_binaria.b ->
  38. (prop_antisimmetria)[prop_antisimmetria/false]) =
  39. (relazione_binaria[i] != relazione_binaria[i].b -> false) = vero
  40. vero and vero = vero
  41.  
  42.  
  43.  
  44.  
  45. La postcondizione Ŕ vera
  46. La precondizione Ŕ vera


Ultima modifica effettuata da julver il 27/01/2015 alle 13:45
PM Quote