- 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
| | Egenskaberne af et muligt specifikationsssprog er direkte inspireret af det objekt-orienterede programmeringssprog
Eiffel Årsagen til, at kvantorer er problematisk, er udtryk for er ønsket om at kunne efterchecke
assertions i et kørende program. Hvis vi ønsker 'kvantorudtryksform' kan vi falde tilbage
på at programmere boolske funktioner, som returnerer hvorvidt 'alle ... opfylder en betingelse' eller
'om der eksisterer ... der opfylder en betinglse' Programmerede udsagn er problematiske derved, at specifikationen ikke ønskes afhængiggjort af programmet.
Hvad skal vi f.eks. stille op med specifikationen af de programmerede udsagn; og hvad hvis der er fejl
i disse dele af programmet? |