Un esempio

float sqrt (float coef) {

// REQUIRES: coef > 0

// EFFECTS: ritorna una approssimazione

// della radice quadrata di coef

float ans = coef / 2.0; int i = 1;

while (i < 7) {

ans = ans-((ans*ans-coef)/(2.0*ans));

i = i+1; }

return ans; }

• precondizione (asserzione requires)

  • deve essere verificata quando si chiama la procedura

• postcondizione (asserzione effects)

  • tutto ciò che possiamo assumere valere quando la chiamata di procedura termina, se al momento della chiamata era verificata la precondizione

Previous slide

Next slide

Back to first slide

View graphic version