Postcondition

Postcondition

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.

ee also

*Precondition
*Design by contract
*Hoare logic
*Invariants maintained by conditions
*Database trigger


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать реферат

Look at other dictionaries:

  • postcondition — posąlygis statusas T sritis informatika apibrėžtis ↑Loginis reiškinys, parašytas po kurio nors programos ↑sakinio (sakinių grupės), kurio reikšmė turi būti ↑tiesa atlikus tą sakinį (sakinių grupę). atitikmenys: angl. postcondition ryšiai: dar… …   Enciklopedinis kompiuterijos žodynas

  • postcondition — noun A condition that must be met immediately after execution of some piece of code …   Wiktionary

  • postcondition — ● n. f. ►PROG assertion placée dans le code source de sorte qu elle soit évaluée juste avant un point de sortie de fonction [NM] …   Dictionnaire d'informatique francophone

  • Eiffel (programming language) — Infobox programming language name = Eiffel paradigm = object oriented year = 1986 designer = Bertrand Meyer developer = Bertrand Meyer Eiffel Software latest release version = 4.2 latest release date = Feb 6, 1998 typing = static typing, strong… …   Wikipedia

  • Monitor (synchronization) — In concurrent programming, a monitor is an object or module intended to be used safely by more than one thread. The defining characteristic of a monitor is that its methods are executed with mutual exclusion. That is, at each point in time, at… …   Wikipedia

  • SPARK (programming language) — infobox programming language name = SPARK influenced by = Ada, HAL/SSPARK is a formally defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software… …   Wikipedia

  • Programmation par contrat — La programmation par contrat est un paradigme de programmation dans lequel le déroulement des traitements est régi par des règles. Ces règles, appelées des assertions, forment un contrat qui précise les responsabilités entre le client et le… …   Wikipédia en Français

  • Design by contract — (DbC) or Programming by Contract is an approach to designing computer software. It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary… …   Wikipedia

  • Assertion (computing) — In computer programming, an assertion is a predicate (i.e., a true–false statement) placed in a program to indicate that the developer thinks that the predicate is always true at that place. For example, the following code contains two assertions …   Wikipedia

  • Precondition — In logic a precondition is a condition that has to be met before a main argument can have any value. 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… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”