Implementing a priority queue
For our queue implementation, the following invariant holds. If the out
list is empty, the in
list has to be empty (that is, the entire queue is empty). During the pivot step, the invariant is temporarily violated and then restored:
scala> case class Fifo(out: List[Int], in: List[Int]) { | | def check(): Boolean = (out, in) match { | case (Nil, x :: xs) => false | case _ => true | } | require(check, "Invariant Failed - out.em") | } defined class Fifo
Note the use of the require
method to make sure the invariant always holds. We use a method called check
; this method, in turn, uses pattern matching to check both the lists.
Here's the first clause:
case (Nil, x :: xs) => false
This clause matches when the out
list is empty and the in
list is non-empty, that is, it has at least one element. We know this violates our invariant and the object construction...