Lecture overview -- Keyboard shortcut: 'u'  Previous page: Specifikation med pre- og postbetingelser [Section] -- Keyboard shortcut: 'p'  Next page: Eksempel på brug af pre- og postbetingelser i et objekt-orienteret program -- Keyboard shortcut: 'n'  Lecture notes - all slides and notes together  slide -- Keyboard shortcut: 't'  Help page about these notes  Alphabetic index  Course home  Play sound for this page -- Keyboard shortcut: 'y'  Page 6 : 31
Forelæsningsnoter i Objekt-orienteret Programmering
Designkontrakter og ansvarsfordeling
Logiske udtryk samt pre- og postbetingelser

Pre- og postbetingelser er rygraden i axiomatiske specifikationer

Et logisk udtryk er et udtryk af typen boolean

En prebetingelse af en operation er et logisk udtryk, som skal være opfyldt umiddelbart før operationen kaldes

En postbetingelse af en operationer et logisk udtryk, som skal være opfyldt umiddelbart efter at operation er udført

'Logiske udtryk' er betegnelsen for den delmængde af udtryk som beregnes til et boolsk resultat (altså true eller false resultat). Et logisk udtryk kaldes også ofte for et udsagn

En prebetingelse er et udsagn om situationen før kaldet af en operation. I prebetingelsen er der mulighed og behov for at referere til operationens parametre

En postbetingelse er et udsagn om situationen efter kaldet af operationen. Hvis operationen er en procedure karakteriserer postbetingelsen programtilstanden efter operationskaldet. Hvis operationen er en funktion beskriver postbetingelsen resultatet (output) i forhold til parametrene (input)

  • Prebetingelse

    • En prebetingelse udtrykker, om det er meningsfyldt at kalde operationen med de givne parametre

    • Prebetingelsen's opfyldelse er en forudsætning for at operationen kan kaldes

  • Postbetingelse

    • En postbetingelse udtrykker at operationen returnerer et bestemt resultat eller har en bestemt effekt, når denne kaldes med de givne parametre som opfylder prebetingelsen

    • Postbetingelsen fastlægger betydningen af operationen

Logiske udtryk kaldes ofte for assertions på engelsk og udsagn på dansk