andrea9671 (Normal User)
Newbie
Messaggi: 5
Iscritto: 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++ |
do
{
n_valori = scanf("%d",
&scelta);
if (n_valori != 1 && (scelta != 0 || scelta != 1))
{
printf("Errore!\n");
while(getchar() != '\n');
}
} while((n_valori != 1) &&
(scelta != 0 ||
scelta != 1));
|
Grazie
|
|
|
andrea9671 (Normal User)
Newbie
Messaggi: 5
Iscritto: 11/01/2016
|
up
|
|
|
Trusted (Normal User)
Newbie
Messaggi: 14
Iscritto: 06/09/2015
|
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! 
Ultima modifica effettuata da Trusted il 17/01/2016 alle 15:48 |
|
|
andrea9671 (Normal User)
Newbie
Messaggi: 5
Iscritto: 11/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 
|
|
|
Trusted (Normal User)
Newbie
Messaggi: 14
Iscritto: 06/09/2015
|
Codice sorgente - presumibilmente Plain Text |
funzione controllavalore(valore)
valoreRiferimento = lettera
se valore non sarà uguale a lettera
#codice qua se valore non corrisponde
se valore sarà uguale a lettera
#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.
|
|
|
andrea9671 (Normal User)
Newbie
Messaggi: 5
Iscritto: 11/01/2016
|
Ciao ascolta, diciamo che sto capendo meglio, volevo chiederti un'ultima cosa, prendendo questo codice:
Codice sorgente - presumibilmente Delphi |
if (n2.forma == ALGEBRICA) { /* verifico se la parte reale o quella immaginaria sono uguali a zero, in tal caso, significa che si verificherà una divisione per zero */ if (n2.valore_t.valore_alg.parte_reale == 0 || n2.valore_t.valore_alg.parte_immaginaria == 0) { divisione_per_zero = TRUE; } } else { /* verifico che il modulo se il modulo è uguale a zero, in tal caso, significa che si verificherà una divsione per zero */ if (n2.valore_t.valore_tri.modulo == 0) { divisione_per_zero = TRUE; } }
|
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 |
|
|
Trusted (Normal User)
Newbie
Messaggi: 14
Iscritto: 06/09/2015
|
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
|
|
|
andrea9671 (Normal User)
Newbie
Messaggi: 5
Iscritto: 11/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++ |
double new_arg = fmod(argomento,2_PI_GRECO);
if(new_arg < 0)
{
new_arg = 2_PI_GRECO + new_arg;
}
|
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 |
|
|
