OOPM1617 Übungswoche 07 (12.12-18.12.16)
Zielsetzung für die Übung
- Besprechung der Hausaufgabe aus letzter Woche
- Testen
- Spezifikation abstrakter Datentypen
Präsenzaufgabe:
Spezifizieren Sie einen Keller "LimitedStack" mit Größenbeschränkung. Verwenden Sie dazu die Spezifikation von Stack als Vorlage. Berücksichtigen Sie dabei, dass das Hinzufügen eines Elements nach Erreichen der Größenbeschränkung ohne Wirkung bleiben soll.
Lösung:
// Stacks -- a LIFO containter
specification stack
imports
bool
nat
nat1
sorts
Elem
Stack
constructors
empty : Nat1 -> Stack
push : Elem x Stack -> Stack
functions
top : Stack -> Elem? // Top-most element
pop : Stack -> Stack? // Stack without top-most element
isEmpty : Stack -> Bool // Test for empty stack
length : Stack -> Nat // Number of elements on the stack
getMaxLength : Stack -> Nat1
variables
e : Elem
s : Stack
n : Nat1
equations
top(push(e, s)) =
if getMaxLength(s) > length(s)
then e
else top(s)
pop(push(e, s)) =
if getMaxLength(s) > length(s)
then s
else pop(s)
isEmpty(empty(n)) = true
isEmpty(push(e, s)) = false
length(empty(n)) = zero
length(push(e, s)) =
if getMaxLength(s) > length(s)
then succ(length(s))
else length(s)
getMaxLength(empty(n)) = n
getMaxLength(push(e,s)) = getMaxLength(s)
Zielsetzung für das Programmierpraktikum
- Implementation abstrakter Datentypen
- Anwendung der funktionalen und imperativen Strategie zur Implementation einer Spezifikation
page revision: 2, last edited: 13 Dec 2016 16:55