OOPM1718 Übungswoche 05 (11.12-17.12.17)

Zielsetzung für die Übung

Spezifikation abstrakter Datentypen

Spezifikation abstrakter Datentypen aus Github

Spezifikation einer Queue mit Größenbeschränkung:

// Queues -- a FIFO containter
imports
  bool
  nat
  nat1
sorts
  Elem
  LimitedQueue
hidden constructors 
  empty' : Nat1 -> LimitedQueue
  enqueue' : Elem x LimitedQueue -> LimitedQueue
functions
  front : LimitedQueue -> Elem? // Front element
  dequeue : LimitedQueue -> LimitedQueue? // LimitedQueue without front element
  isEmpty : LimitedQueue -> Bool // Test for empty LimitedQueue
  length : LimitedQueue -> Nat // Number of elements in the LimitedQueue
  isMaxErreicht : LimitedQueue -> Bool
  getMax : LimitedQueue -> Nat1
  enqueue : Elem x LimitedQueue -> LimitedQueue
variables
  e : Elem
  e1 : Elem
  e2 : Elem
  q : Queue
  n : Nat1
equations
  front(enqueue'(e, empty'(n))) = e
  front(enqueue'(e1, enqueue'(e2, q))) = front(enqueue'(e2, q))
  dequeue(enqueue'(e, empty'(n))) = empty'(n)
  dequeue(enqueue'(e1, enqueue'(e2, q))) = enqueue'(e1, dequeue(enqueue'(e2, q)))
  isEmpty(empty'(n)) = true
  isEmpty(enqueue'(e, q)) = false
  length(empty'(n)) = zero
  length(enqueue'(e, q)) = succ(length(q))

  enqueue(e1, empty'(n)) = enqueue'(e1, empty'(n))
  enqueue(e1, enqueue'(e,q)) = 
    if isMaxErreicht(enqueue'(e,q))
      then enqueue'(e,q)
      else enqueue'(e1, enqueue'(e,q))

  isMaxErreicht(empty'(n)) = false
  isMaxErreicht(enqueue'(e,q)) = 
    if succ(length(q)) < getMax(q) 
      then false 
      else true

  getMax(empty'(n)) = n
  getMax(enqueue'(e,q)) = getMax(q)

Zielsetzung für das Programmierpraktikum

Implementation abstrakter Datentypen