Et sprog til formulering af 'assertions'

Stop show with sound -- Keyboard shortcut: 'x'

Next slide in show -- Keyboard shortcut: 'n'

4 minutes, 16 seconds

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