Testing dei cammini nella specifica
un buon modo di generare dati di test è di esplorare cammini alternativi attraverso la specifica
- i cammini si possono trovare mediante le clausole REQUIRES e EFFECTS
inoltre vanno testati
- i casi limite
- gli errori di aliasing