Una precondizione è una condizione applicata all'inizio di un calcolo o di una funzione del computer e che consente la convalida del risultato.
Se P è un predicato e S una sostituzione, P | S, che recita: il predicato P precondiziona la sostituzione S, è definito da:
[P | S] I ⟺ P & [S] Iche recita:
Sostituzione condizionata [P | S] stabilisce I se e solo se P e la sostituzione ("e" logica) S stabilisce che I è vero.
A causa di &, se la precondizione P è falsa, P & [S] I è falsa.
P | S ha una forma sintattica:
PRE P THEN S END