Et sprog til formulering af 'assertions'

Play audio slide show -- Keyboard shortcut: 'x'

Lecture overview -- Keyboard shortcut: 'u'

Previous page: Eksempel på brug af pre- og postbetingelser i et objekt-orienteret program -- Keyboard shortcut: 'p'

Next page: Ansvarsfordeling og kontrakter [Section] -- Keyboard shortcut: 'n'

Lecture notes - all slides and notes together

Annotated slide -- Keyboard shortcut: 't'

Alphabetic index

Help page about these notes

Play sound for this slide -- Keyboard shortcut: 'y'

Designkontrakter og ansvarsfordeling - slide 8 : 31

Et sprog til formulering af 'assertions'

Vi ønsker at inkludere en specifikation i termer af pre- og postbetingelser i et program

Vi må have et delsprog af programmeringssproget, i hvilket vi kan formulere 'assertions' i et program

Vi ønsker at kunne efterchecke udsagn i et kørende program

Et muligt specifikationssprog
- Understøttelse af simple, logiske udtryk (med and, or, not, implies)
- Brug af alkvantorer ('for alle ...') og eksistenskvantorer ('der eksisterer ...')
  - Det er problematisk at efterchecke udtryk med kvantorer i et kørende program
- Understøttelse af programmerede assertions via boolske funktioner i programmeringssproget
  - Problematisk hvis der er fejl i disse
- Understøttelse af uformelt formulerede udsagn i programkommentarer
  - Langt bedre end ingen specifikation