Précondition
Cet article est une ébauche concernant les mathématiques et la logique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
Une précondition est une condition appliquée au début d'un calcul ou d'une fonction informatique, et permettant d'en valider le résultat.
Expression B de précondition
Si P est un prédicat et S une substitution, P | S, qui se lit : le prédicat P préconditionne la substitution S, est défini par :
[P | S] I ⟺ P & [S] I
qui se lit :
La substitution conditionnée [P | S] établit I si et seulement si P et ("et" logique) la substitution S établit que I est vrai.
Du fait du &, si la précondition P est fausse, P & [S] I est faux.
P | S a une forme syntaxique :
PRE P THEN S END
Articles connexes
- Programmation par contrat
- Portail des mathématiques
- Portail de la logique