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.

PropertyValue
dbpprop:abstract
  • 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.
  • Die Nachbedingungen einer Funktion oder eines Programms geben an, welche Aussagen nach der Ausführung gelten müssen, falls zuvor die Vorbedingungen erfüllt waren. Die Nachbedingung ist Teil der formalen Spezifikation der Funktion (bzw. des Programms) und dient der Verifikation: Wenn die Vorbedingung gilt, so müssen nach Ausführung der Funktion alle Nachbedingungen erfüllt sein, sonst ist das Programm nicht korrekt. Das Konzept von Vor- und Nachbedingungen wird vor allem in der formalen Semantik benutzt: es stellt die Basis der axiomatischen Semantik dar. Das Ziel ist es dabei, aus den Vor- und Nachbedingungen der einzelnen Teile des Programms logisch die gewünschte Nachbedingung für das gesamte Programm zu folgern. Auch bei dem weniger formalen Testen von Software spielen Nachbedingungen eine wesentliche Rolle, da das Ergebnis von Testläufen leicht mit den Nachbedingungen verglichen werden kann. Das wird vor allem für den so genannten Unit-Test verwendet.
  • En programación, una postcondición es una condición o predicado lógico que siempre debe cumplirse justamente después de la ejecución de una sección de código o de una operación. Las postcondiciones se prueban a veces mediante aserciones incluidas en el código. A menudo, las postcondiciones se incluyen simplemente en la documentación de la correspondiente sección de código. Por ejemplo: el resultado de un factorial es siempre un entero mayor o igual que 1. De este modo un programa que calcula el factorial de un número dado tendría como postcondiciones que el resultado debe ser un entero y que éste debe ser mayor o igual que 1.
  • Пі́сляумова, в програмуванні та формальних методах — правило відносно результатів виконання функції, яке має виконуватись, якщо було виконано вимоги передумови. Післяумова є складовою частиною формальної специфікації функції і використовується для її верифікації: в разі виконання передумов, мусять, відповідно, виконуватись і всі післяумови, в іншому випадку, функція не коректна. Післяумови, відіграють, також, важливу роль і в менш формальному тестуванні, оскільки легко можна порівняти результати тестів із післяумовами. Такий підхід використовується в так званих модульних тестах.
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • 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.
  • Die Nachbedingungen einer Funktion oder eines Programms geben an, welche Aussagen nach der Ausführung gelten müssen, falls zuvor die Vorbedingungen erfüllt waren. Die Nachbedingung ist Teil der formalen Spezifikation der Funktion (bzw. des Programms) und dient der Verifikation: Wenn die Vorbedingung gilt, so müssen nach Ausführung der Funktion alle Nachbedingungen erfüllt sein, sonst ist das Programm nicht korrekt.
  • En programación, una postcondición es una condición o predicado lógico que siempre debe cumplirse justamente después de la ejecución de una sección de código o de una operación. Las postcondiciones se prueban a veces mediante aserciones incluidas en el código. A menudo, las postcondiciones se incluyen simplemente en la documentación de la correspondiente sección de código. Por ejemplo: el resultado de un factorial es siempre un entero mayor o igual que 1.
  • Пі́сляумова, в програмуванні та формальних методах — правило відносно результатів виконання функції, яке має виконуватись, якщо було виконано вимоги передумови.
rdfs:label
  • Postcondition
  • Nachbedingung (Informatik)
  • Postcondición
  • Післяумова (формальні методи)
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of