Précondition

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

 

Prefix: a b c d e f g h i j k l m n o p q r s t u v w x y z 0 1 2 3 4 5 6 7 8 9

Portal di Ensiklopedia Dunia