|
|
Logiske udtryk samt pre- og postbetingelser | Pre- og postbetingelser er rygraden i axiomatiske specifikationer |
| '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) |
|
|
|