Object Oriented Queue

Applications
1

I was told to writeup what an OO queue is, so here we go

interface ITuple = {
  first : any
  second : any
}

interface IQueue = {
   enqueue : IQueue -> any -> IQueue
   pop : IQueue -> IQueue
   first : IQueue -> any
   empty? : IQueue -> Bool
   ;; dequeue : IQueue -> ITuple(IQueue, any)
   ;; can be implemented by doing pop and first
}

Tuple(f, s) µ this. {
   first = f
   second = s
}

Empy_Queue µ this. {
  enqueue = λa. Cons_Queue(a, this)
  pop = nil
  first = nil
  empty? = true
}

Cons_Queue(item, queue)  µ this. {
  enqueue = λa. Cons_Queue(a, this)
  pop = if empty?(queue) then queue else Cons_Queue(item, pop(queue))
  first = if empty?(queue) then item else first(queue)
  empty? = false
}

This should be a correct and complete implementation of an OO queue.

We made two objects, one which is the empty_queue which is always empty, and a cons_queue that can cons items.

If so desired I can implement this in logtalk and have it actually run

1 Like
2

The exercise is then to see if there is a suitable way of specify what correct means for OO using logic a la coCASL while the axiomatization for ADTs is common knowledge..

3

I’m confused, the link for which it is in common knowledge for seems to covering C++, we can just assert like that page exist that those properties are true, and to be a non faulty implementation of Queue those properties must hold. Much like CPP we can assume these as axioms if you want to prove it, then it’s much the same way as proving things for the sort. Given the body you show the axioms hold up, in this case it’s trivial for Empty_Queue and Cons_Queue to show all those properties exist if we were writing this in a language which can prove properties as all constructors and their properties are known.

Thus the prove for Cons_Queue holds if the proofs hold inductively for the queue parameter and so on and so forth