Testing dei cammini nella specifica 1
esempio di cammino nella clausola REQUIRES
- specifica di un metodo stand alone
static float sqrt (float x, float epsilon)
// REQUIRES: X >= 0 & .00001 < epsilon < .001
// EFFECTS: ritorna sq tale che x - epsilon <= sq*sq <= x + epsilon
la clausola REQUIRES in forma disgiuntiva
(x = 0 | x > 0) & .00001 < epsilon < .001 =
1. (x = 0 & .00001 < epsilon < .001) |
2. (x > 0 & .00001 < epsilon < .001)
un insieme di dati di test per sqrt deve controllare ciascuno di questi due casi