Precondition

The condition required of a starting program state for a stated correctness guarantee. In the summation loop verification,

n \in Z

and

n \geq 0

admit

n = 0

and

n = 4

, but exclude

n = - 1

. The accompanying model assumes exact integer arithmetic and terminating elementary operations. The initial values of

i, s

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

n \geq 0

here makes

n = - 2

a terminating counterexample to

2 s = n (n + 1)

, since initialization returns zero while

n (n + 1) = 2

 Ancestors (6)

 Incoming links (116)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (1)

Precondition by

Wikipedia Bot  1

 View more

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.

 Read the full article

  See all articles in the same topic Create my own version

Precondition

 Ancestors (6)

 Incoming links (116)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (1)

 Discussion (0) New discussion