Spécification : contrat ?
Une signature ne spécifie pas un service !
- on garantit seulement que l'appel et les résultats sont correctement typés montant déposer(in montant somme);
Introduction de précondition et de postcondition
montant déposer(in montant somme) {require somme > 0} {ensure solde = old solde + somme};