What are preconditions and postconditions?

Question

I'm learning how to program but one thing I can't quite get my head around is preconditions and postconditions.

Is an if statement before calling a function considered a precondition, or is there a separate more efficient way of doing this in most languages?

I'm also struggling to find any examples of preconditions that I could understand with my current knowledge of programming if anyone could prove a simple one then I would really appreciate it (any language will be fine)

Answer 1

This is a computer science question, not a programming question, so it would be more appropriate on https://cs.stackexchange.com/, but I'll answer it anyway.

Consider this program to find the first index of a needle in a haystack. (The haystack might contain many needles; we want to stop at the first one.) If the haystack doesn't contain a needle, the index is equal to the size of the haystack (which is not a valid index into the haystack).

i = 0
while i < haystack.count && haystack[i] != needle {
    i = i + 1
}

A “postcondition” is an assertion about the state of a program that, typically, says the program has computed something useful (at the point of the postcondition). For the example program, we can write postconditions asserting that it computed the result we want:

i = 0
while i < haystack.count && haystack[i] != needle {
    i = i + 1
}
assert(i == haystack.count || haystack[i] == needle) // first postcondition
haystack[0 ..< i].forEach { assert($0 != needle) } // second postcondition

(Note: 0 ..< i means all j such that 0 ≤ j < i.)

The first postcondition asserts that either i is the number of items in the haystack, or i is the index of a needle.

The second postcondition asserts that a needle doesn't appear in the haystack anywhere earlier than index i. Therefore the program found the first needle, if it found any needle.

Thus if these postconditions are true, the program did what we wanted.

A “precondition” is an assertion about the state of the program that, when combined with the program's subsequent actions, can be used to prove the postconditions. We can add preconditions to our example program:

i = 0
while i < haystack.count && haystack[i] != needle {
    haystack[0 ... i].forEach { assert($0 != needle) } // precondition
    i = i + 1
}
assert(i == haystack.count || haystack[i] == needle) // first postcondition
haystack[0 ..< i].forEach { assert($0 != needle) } // second postcondition

(Note: 0 ... i means all j such that 0 ≤ j ≤ i.)

The precondition tells us that all of the haystack elements up to and including the element at index i are not the needle.

You can use induction to prove that the precondition is true every time the program reaches it. The loop ends when its condition is false, which means the first postcondition is true. (The first postcondition is the contrapositive of the loop condition.) The fact that the loop precondition was true means that the second postcondition is also true.

Answer 2

That's the wrong way of doing that math with this individual. First the variables aren't all there and the solution loop is incorrect due to the simple fact of missing variables . Furthermore because of said missing variables and instability in the actual equation you cannot get a solution to this equation without a double blind study and 1 absolute variable. Which insequently voids the point of your equation to begin with. Lastly as that I happen to be a magic wielding semi intelligent smart ass I could argue that if one wishes to find a needle in a haystack one would simply light a match and wait. When said haystack is gone use a magnet. Problem solved no math.

Answer 3

It is well-stated in this c++'s paper

• A precondition is a predicate that should hold upon entry into a function. It expresses a function's expectation on its arguments and/or the state of objects that may be used by the function.

• A postcondition is a predicate that should hold upon exit from a function. It expresses the conditions that a function should ensure for the return value and/or the state of objects that may be used by the function.

---

Preconditions and postconditions belong to Contract-based-programming.

In Dlang, Contract-based-programming have good designs. This document offers a sample:

long square_root(long x)
in
{
    assert(x >= 0);
}
out (result)
{
    assert(result ^^ 2 <= x && (result + 1) ^^ 2 > x);
}
do
{
    return cast(long)std.math.sqrt(cast(real)x);
}

Preconditions are in in block, postconditions are in out block.

• If preconditions and postconditions are satisfied, then it will compile happily, like passing 9 into the function. live demo
• If preconditions are not satisfied, like passing -1 into the function. live demo

  [email protected](8): Assertion failure

• If postconditions are not satisfied which can be caused by we didn't deal with the logic in the do block, like return square rather than square-root, then, postconditions will work: live demo

  [email protected](13): Assertion failure

For class, Dlang also has good tools, read the document to learn more

---

BTW, c++ also lists contract design into c++20's draft: https://www.reddit.com/r/cpp/comments/8prqzm/2018_rapperswil_iso_c_committee_trip_report/

Here is the proposal, maybe also helpful to understand them(though, much ugly than D, IMHO)