Lecture overview -- Keyboard shortcut: 'u'  Previous page: Korrekthed -- Keyboard shortcut: 'p'  Next page: Specifikation med pre- og postbetingelser [Section] -- 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 4 : 31
Forelæsningsnoter i Objekt-orienteret Programmering
Designkontrakter og ansvarsfordeling
Specifikation

Specifikation går forud for implementation. Vi kan opfatte specifikation som en del af designfasen. Her ser vi på forskellige aspekter af specifikationer

En program specifikation er en eksakt forskrift som skal opfyldes af program implementationen

En specifikation besvarer 'hvad spørgsmål' i modsætning til 'hvordan spørgsmål'

En specifikation beskriver og foreskriver egenskaberne af en efterfølgende program implementation. Ideelt beskæftiger en specifikation sig med 'hvad' et program skal gøre, ikke noget om 'hvordan' det skal ske

  • Formelle teknikker til specifikation af abstrakte datatyper:

    • Algebraisk specifikation. En mængde af ligninger som angiver de kaldsmæssige egenskaber af datatypens operationer i forhold til et antal særlige konstruktorer

    • Axiomatisk specifikation. En mængde af logiske udsagn om de definitionsmæssige egenskaber af datatypen og dens operationer

Algebraisk specifikation er en elegant teknik, som tillader os at specificere abstrakte datatyper. Kerneideen er en angivelse af, hvordan de forskellige operationer (funktioner) virker på såkaldte konstruktorer (også funktioner)

I denne lektion vil vi koncentrere os om axiomatiske specifikationer

/user/normark/courses/prog1/prog1-01/sources/noter/includes/stack-specificationEt eksempel på en algebraisk specifikation af en stak.

Et eksempel på en algebraisk specifikation af en stak. Øverst ser vi en syntaktisk definition af signaturerne af de operationer, som virker på en stak. Alle operationer skal være funktioner. Nederst ses den semantiske specifikation af stakken. Princippet er at vise hvordan de forskellige stakfunktioner virker på konstruktorerne, som er new og push.

/user/normark/courses/prog1/prog1-01/sources/noter/includes/kvadratrods-specificationEt eksempel på en axiomatisk specifikation af en kvadratrodsfunktion.

Et eksempel på en axiomatisk specifikation af en kvadratrodsfunktion.