(of a statement S in some program) An assertion that characterizes the state of the program immediately prior to execution of S. The precondition is expressed in terms of properties of certain program variables and relationships between them. Where a program text is annotated by attaching assertions, a precondition is attached immediately before the statement to which it relates. For a consistent annotation the precondition of S must be implied by the postcondition of any statement whose execution can immediately precede execution of S. See also weakest precondition.