Il punto di vista di chi usa la procedura
float sqrt (float coef) {
// EFFECTS: ritorna una approssimazione
// della radice quadrata di coef
- gli utenti della procedura non si devono preoccupare di capire cosa la procedura fa, astraendo le computazioni descritte dal corpo
- cosa che può essere molto complessa
- gli utenti della procedura non possono osservare le computazioni descritte dal corpo e dedurre da questo proprietà diverse da quelle specificate dalle asserzioni
- astraendo dal corpo (implementazione), si “dimentica” informazione evidentemente considerata non rilevante