In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself. Often, postconditions are simply included in the documentation of the affected section of code.
For example: The result of a factorial is always an integer and greater than or equal to 1. So a program that calculates the factorial of an input number would have postconditions that the result after the calculation be an integer and that it be greater than or equal to 1. Another example: a program that calculates the square root of an input number might have the postconditions that the result be a number and that its square be equal to the input.
In some software design approaches, postconditions, along with preconditions and class invariants, are components of the software construction method design by contract.
The postcondition for any routine is a declaration of the properties which are guaranteed upon completion of the routine's execution.[1] As it relates to the routine's contract, the postcondition offers assurance to potential callers that in cases in which the routine is called in a state in which its precondition holds, the properties declared by the postcondition are assured.
Eiffel example
The following example written in Eiffel sets the value of a class attribute hour based on a caller-provided argument a_hour. The postcondition follows the keyword ensure. In this example, the postcondition guarantees, in cases in which the precondition holds (i.e., when a_hour represents a valid hour of the day), that after the execution of set_hour, the class attribute hour will have the same value as a_hour. The tag "hour_set:" describes this postcondition clause and serves to identify it in case of a runtime postcondition violation.
set_hour(a_hour:INTEGER)-- Set `hour' to `a_hour'requirevalid_argument:0<=a_houranda_hour<=23dohour:=a_hourensurehour_set:hour=a_hourend
Postconditions and inheritance
In the presence of inheritance, the routines inherited by descendant classes (subclasses) do so with their contracts, that is their preconditions and postconditions, in force. This means that any implementations or redefinitions of inherited routines also have to be written to comply with their inherited contracts. Postconditions can be modified in redefined routines, but they may only be strengthened.[2] That is, the redefined routine may increase the benefits it provides to the client, but may not decrease those benefits.
postcondition, computer, programming, postcondition, condition, predicate, that, must, always, true, just, after, execution, some, section, code, after, operation, formal, specification, sometimes, tested, using, assertions, within, code, itself, often, postco. In computer programming a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification Postconditions are sometimes tested using assertions within the code itself Often postconditions are simply included in the documentation of the affected section of code For example The result of a factorial is always an integer and greater than or equal to 1 So a program that calculates the factorial of an input number would have postconditions that the result after the calculation be an integer and that it be greater than or equal to 1 Another example a program that calculates the square root of an input number might have the postconditions that the result be a number and that its square be equal to the input Contents 1 Postconditions in object oriented programming 2 Eiffel example 3 Postconditions and inheritance 4 See also 5 ReferencesPostconditions in object oriented programming EditIn some software design approaches postconditions along with preconditions and class invariants are components of the software construction method design by contract The postcondition for any routine is a declaration of the properties which are guaranteed upon completion of the routine s execution 1 As it relates to the routine s contract the postcondition offers assurance to potential callers that in cases in which the routine is called in a state in which its precondition holds the properties declared by the postcondition are assured Eiffel example EditThe following example written in Eiffel sets the value of a class attribute hour based on a caller provided argument a hour The postcondition follows the keyword ensure In this example the postcondition guarantees in cases in which the precondition holds i e when a hour represents a valid hour of the day that after the execution of set hour the class attribute hour will have the same value as a hour The tag hour set describes this postcondition clause and serves to identify it in case of a runtime postcondition violation set hour a hour INTEGER Set hour to a hour require valid argument 0 lt a hour and a hour lt 23 do hour a hour ensure hour set hour a hour endPostconditions and inheritance EditIn the presence of inheritance the routines inherited by descendant classes subclasses do so with their contracts that is their preconditions and postconditions in force This means that any implementations or redefinitions of inherited routines also have to be written to comply with their inherited contracts Postconditions can be modified in redefined routines but they may only be strengthened 2 That is the redefined routine may increase the benefits it provides to the client but may not decrease those benefits See also EditPrecondition Design by contract Hoare logic Invariants maintained by conditions Database triggerReferences Edit Meyer Bertrand Object Oriented Software Construction second edition Prentice Hall 1997 p 342 Meyer 1997 pp 570 573 Retrieved from https en wikipedia org w index php title Postcondition amp oldid 1061639236, wikipedia, wiki, book, books, library,
