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++ - Problema triple di Hoare
Forum - C/C++ - Problema triple di Hoare

Avatar
andrea9671 (Normal User)
Newbie


Messaggi: 5
Iscritto: 11/01/2016

Segnala al moderatore
Postato alle 16:56
Lunedì, 11/01/2016
Salve a tutti, volevo chiedermi come posso dimostrare con le triple di hoare la correttezza del seguente segmento di codice

Codice sorgente - presumibilmente C/C++

  1. do
  2.         {
  3.                 n_valori = scanf("%d",
  4.                                  &scelta);
  5.  
  6.  
  7.                 if (n_valori != 1 && (scelta != 0 || scelta != 1))
  8.                 {
  9.                         printf("Errore!\n");
  10.                         while(getchar() != '\n');
  11.                 }
  12.                
  13.         } while((n_valori != 1) &&
  14.                 (scelta != 0 ||
  15.                  scelta != 1));



Grazie

PM Quote
Avatar
andrea9671 (Normal User)
Newbie


Messaggi: 5
Iscritto: 11/01/2016

Segnala al moderatore
Postato alle 14:00
Domenica, 17/01/2016
up

PM Quote
Avatar
Trusted (Normal User)
Newbie


Messaggi: 14
Iscritto: 06/09/2015

Segnala al moderatore
Postato alle 15:47
Domenica, 17/01/2016
Ciao!

Sai come funziano le triple di Hoare? se <Z> è il tuo codice devi trovare una pre-condizione <N> ed una post-condizione <M> che ne garantiscano il successo. Ad esempio una pre-condizione sarebbe verificare che i dati immessi siano effettivamente numeri e non caratteri alfanumerici.
Mentre una post-condizione dovrebbe verificare che i numeri corrispondano a quelli previsti.

Bella pè te! :k:

Ultima modifica effettuata da Trusted il 17/01/2016 alle 15:48


Io oso tutto ciò che è degno di un uomo, chi osa di più non lo è.
PM Quote
Avatar
andrea9671 (Normal User)
Newbie


Messaggi: 5
Iscritto: 11/01/2016

Segnala al moderatore
Postato alle 13:39
Lunedì, 18/01/2016
Grazie intanto per la risposta, si so come funziona una tripla di hoare, ma la cosa che non riesco a fare e passare dal codice ad una precondizione o postcondizione, potresti farmi un esempio?

Grazie :)

PM Quote
Avatar
Trusted (Normal User)
Newbie


Messaggi: 14
Iscritto: 06/09/2015

Segnala al moderatore
Postato alle 20:02
Giovedì, 21/01/2016
Codice sorgente - presumibilmente Plain Text

  1. funzione controllavalore(valore)
  2.        valoreRiferimento = lettera
  3.        
  4.        se valore non sarà uguale a lettera
  5.                 #codice qua se valore non corrisponde
  6.  
  7.         se valore sarà uguale a lettera
  8.                  #codice qua se valore corrisponde




Questo barbarico script in pseudocodice dovrebbe darti una idea di una funzione che svolge il ruolo di pre-condizione <N>

Per "creare" il valore di riferimento puoi usare  typeid http://www.cplusplus.com/reference/typeinfo/type_info/
controlli poi se il tipo di valore, del dato immesso corrisponde e fai seguire il resto del codice, altrimenti lo blocchi.
:k:



Io oso tutto ciò che è degno di un uomo, chi osa di più non lo è.
PM Quote
Avatar
andrea9671 (Normal User)
Newbie


Messaggi: 5
Iscritto: 11/01/2016

Segnala al moderatore
Postato alle 1:29
Sabato, 23/01/2016
Ciao ascolta, diciamo che sto capendo meglio, volevo chiederti un'ultima cosa, prendendo questo codice:

Codice sorgente - presumibilmente Delphi

  1. if (n2.forma == ALGEBRICA)
  2.                 {
  3.                         /* verifico se la parte reale o quella immaginaria sono uguali a zero, in tal caso, significa
  4.                            che si verificherà una divisione per zero */
  5.                         if (n2.valore_t.valore_alg.parte_reale == 0 || n2.valore_t.valore_alg.parte_immaginaria == 0)
  6.                         {
  7.                                 divisione_per_zero = TRUE;
  8.                         }
  9.                 }
  10.                 else
  11.                 {      
  12.                         /* verifico che il modulo se il modulo è uguale a zero, in tal caso,
  13.                            significa che si verificherà una divsione per zero */
  14.                         if (n2.valore_t.valore_tri.modulo == 0)
  15.                         {
  16.                                 divisione_per_zero = TRUE;
  17.                         }
  18.                 }



Quale sarebbe la post-conzione? Ed inoltre da quest'ultima devo risalire alla pre-condiziome, saresti in grado di farmi una dimostrazione completa?

Grazie :)

Ultima modifica effettuata da andrea9671 il 23/01/2016 alle 18:25
PM Quote
Avatar
Trusted (Normal User)
Newbie


Messaggi: 14
Iscritto: 06/09/2015

Segnala al moderatore
Postato alle 11:38
Domenica, 24/01/2016
Beh è abbastanza difficile parlare di pre-condizioni e post-condizioni senza avere in mente il problema. Se stai cercando di controllare gli errori generati da una divisione per 0, con una pre-condizione, dovresti assicurarti che numeratore e denominatore siano diversi da 0.

Poi cosa intendi con "da quest'ultima devo risalire alla pre-condiziome"

Saluti:)


Io oso tutto ciò che è degno di un uomo, chi osa di più non lo è.
PM Quote
Avatar
andrea9671 (Normal User)
Newbie


Messaggi: 5
Iscritto: 11/01/2016

Segnala al moderatore
Postato alle 19:29
Lunedì, 25/01/2016
Grazie mille, comunque ho deciso di prendere questa parte di codice, dove devo calcolare un nuovo argomento in modo tale che sia compreso nel range [0, 2pi_greco]
Codice sorgente - presumibilmente C/C++

  1. double new_arg = fmod(argomento,2_PI_GRECO);
  2. if(new_arg < 0)
  3. {
  4.     new_arg = 2_PI_GRECO + new_arg;
  5. }



Ora data la tripla di hoare {P} S {Q}, dove {Q}, ovvero la postcondizione è:

{0<new_arg<2_PI_GRECO}

quindi la precondizione {2_PI_GRECO +new_arg> 0 /\ 2_PI_GRECO+new_arg > 2_PI_GRECO}
è verificata in quanto {new_arg > -2_PI_GRECO /\ new_arg < 0} e la seconda condzione è verificata dall'if mentre la prima dall'fmod prima dell'if, ore quello che chiedo come posso rappresentare questo ragionamento, con una logica migliore, ovvero scrivendo delle asserzioni corrette ?
Grazie

Ultima modifica effettuata da andrea9671 il 27/01/2016 alle 21:40
PM Quote