Vecchia Spugna
21-06-2005, 21:45
Allora ragazzi devo fare sta cavolo di verifica di correttezza... ho scelto questo pezzetto di codice(il + semplice che potevo trovare nel mio programma) e ho provato ad abbozzare qualcosina.. sui libri di testo l'argomento non è trattato e le lezioni sono state abbastanza inutili
Il segmento di codice preso in considerazione è:
if(occurs >= size/2)
{
result = 1;
}
else
{
result = 0;
}
Il seguente segmento di codice è corretto perchè ha come postcondizione:
result = (isTrue, [occurs >= size/2])
La precondizione più debole risulta essere vero in quanto:
(istrue([occurs >= size/2)] --> wp(assign(result), result=1)
AND
( NOT(istrue[occurs >=size/2)) --> wp(assign(result), result = 0)
e siccome:
wp(assign(result), result) ;
(result = 1)result, 1 ;
(1=1) true;
e
wp(assign(result), result ;
(result = 0)result, 1 ;
(0=0) true;
risulta che
true --> true AND false --> true
quindi
true AND true = TRUE
alloooooooora considerazioni mie: la prima postcondizione mi puzza un bel pò... poi altro non saprei veramente... ho davvero difficoltà a trovare informazioni su sto argomento. se qualcuno ha conoscenza in materia lo ringrazio di cuore
ciao a tutti belli(io) e brutti(voi)
dimenticavo.. wp = precondizione più debole
Il segmento di codice preso in considerazione è:
if(occurs >= size/2)
{
result = 1;
}
else
{
result = 0;
}
Il seguente segmento di codice è corretto perchè ha come postcondizione:
result = (isTrue, [occurs >= size/2])
La precondizione più debole risulta essere vero in quanto:
(istrue([occurs >= size/2)] --> wp(assign(result), result=1)
AND
( NOT(istrue[occurs >=size/2)) --> wp(assign(result), result = 0)
e siccome:
wp(assign(result), result) ;
(result = 1)result, 1 ;
(1=1) true;
e
wp(assign(result), result ;
(result = 0)result, 1 ;
(0=0) true;
risulta che
true --> true AND false --> true
quindi
true AND true = TRUE
alloooooooora considerazioni mie: la prima postcondizione mi puzza un bel pò... poi altro non saprei veramente... ho davvero difficoltà a trovare informazioni su sto argomento. se qualcuno ha conoscenza in materia lo ringrazio di cuore
ciao a tutti belli(io) e brutti(voi)
dimenticavo.. wp = precondizione più debole