Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What are preconditions and postconditions?

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)

like image 558
Simon J Avatar asked Feb 09 '16 22:02

Simon J


People also ask

What is precondition and postcondition in Java?

The precondition is what the method expects in order to do its job properly. A postcondition is a condition that is true after running the method. It is what the method promises to do. Postconditions describe the outcome of running the method, for example what is being returned or the changes to the instance variables.

What are pre-conditions post-conditions and invariants?

A pre-condition to a function is a condition that must be true before entering the function—no matter what. A post-condition to a function is a condition that must be true before leaving the function—no matter what. A loop invariant is a condition that must be true at the beginning and end of the body of a loop.

What is a postcondition give an example?

A postcondition associated with a method invocation is a condition that must be true when we return from a method. For example, if a natural logarithm method was called with input X, and the method returns Y, we must have (within the limits of the level of precision being used).

What is a precondition in programming?

In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.


1 Answers

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)

like image 94
Chen Li Avatar answered Sep 29 '22 04:09

Chen Li