Oh my god... verifica di correttezza, triple di HOARE help!!

[Vecchia Spugna]

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

[Vecchia Spugna]

uppettino...
raga ignorate? cavolo... sto nuotando nella cacchina....