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