Oopm1516 Ex04
Zielsetzung für die Übung
- Spezifikation für die Priority Queue
- Folgende Spezifikation ist die Zusammentragung aus beiden Dienstags-Übungen
sorts
Elem
PQueue
constructors
empty : -> PQueue
enqueue : Elem x Nat x PQueue -> PQueue
hidden constructor
enqueueAtFront : Elem x Nat x PQueue -> PQueue // the priority is high enough so that the just enqueued element is the front element
functions
front : PQueue -> Elem? // Front element
dequeue : PQueue -> PQueue? // PQueue without front element
isEmpty : PQueue -> Bool // Test for empty Pqueue
length : PQueue -> Nat // Number of elements in the Pqueue
variables
e : Elem
e1 : Elem
e2 : Elem
p : Nat
p1 : Nat
p2 : Nat
q : PQueue
equations
// length(q) = ... können wir nicht sagen. q ist eine beliebige Schlange
length(enqueue(e, p, q)) = succ(length(q))
length(empty()) = zero
isEmpty(empty()) = true
isEmpty(enqueue(e, p, q)) = false
// dequeue(q) = ... können wir nicht sagen
length(dequeue(enqueue(e,p,q))) = length(q)
dequeue(enqueue(e, p, empty())) = empty()
dequeue(enqueueAtFront(e, p, q)) = q
// front(enqueue(e, p, q)) = e ... können wir nicht sagen.
front(enqueueAtFront(e, p, q)) = e
front(enqueue(e, p, empty())) = e
front(enqueue(e2, p2, enqueue(e1, p1, empty()))) =
if greater(p2, p1)
then e2
else e1
enqueue(e, p, empty) = enqueueAtFront(e, p, empty)
enqueue(e1, p1, enqueue(e2, p2, empty())) =
if greater(p1, p2)
then enqueueAtFront(e1, p1, enqueue(e2, p2, empty())))
else enqueueAtFront(e2, p2, enqueue(e1, p1, empty())))
let q2 = enqueue(e1, p1, enqueueAtFront(e2, p2, q)) in
e2 = if greater(p1, p2)
then front(dequeue(q2))
else front(q2)
enqueue(e1, p1, enqueueAtFront(e2, p2, q)) =
if greater(p1, p2)
then enqueueAtFront(e1, p1, enqueueAtFront(e2, p2, q))
else enqueueAtFront(e2, p2, enqueue(e1, p1, q))
Zielsetzung für das Programmierpraktikum
- Umgang mit Feldern (Arrays)
- deklarieren
- initialisieren
- zugreifen
- Iteration über Arrays
- eindimesnsional
- zweidimensional
- Suchen in Arrays
- Sortieren von Arrays
page revision: 3, last edited: 26 Nov 2015 09:52