The condition required of a starting program state for a stated correctness guarantee. In the summation loop verification, and admit and , but exclude . The accompanying model assumes exact integer arithmetic and terminating elementary operations. The initial values of need no restriction because initialization overwrites them before use.
A precondition is a logical assumption, not automatically an executable check. Writing
require in a procedure states its contract; an implementation that checks or rejects invalid inputs needs that behavior specified too. Weakening a precondition admits more starts and therefore demands more proof: dropping here makes a terminating counterexample to , since initialization returns zero while . Articles by others on the same topic
A precondition is a condition or requirement that must be satisfied or fulfilled before a certain action or function can be executed or a particular scenario can take place. In programming and software development, preconditions are often used to specify the necessary state of the system or inputs required for a function or method to perform correctly. For example, in a function that calculates the square root of a number, a precondition might be that the input number must be non-negative.