Use an abstract finite sequence of integers, initially empty. In the following trait, comments are the mathematical specification; means the abstract state on entry, and result means the returned value.
trait ReversableBuffer {
  // Abstract state s: finite sequence of Int, initially [].

  // Pre: true. Post: s = s0 ++ [x].
  def append(x: Int): Unit

  // Pre: true. Post: s = [x] ++ s0.
  def prepend(x: Int): Unit

  // Pre: 0 <= i < length(s0).
  // Post: result = s0 !! i,
  //       s = take i s0 ++ drop (i+1) s0.
  def get(i: Int): Int

  // Pre: true. Post: s = reverse(s0).
  def rev: Unit
}
The postcondition of get includes removal: it is not merely indexed reading. In particular,
(1)
Repeated equal values elsewhere in the sequence remain present. List concatenation, indexing and list reversal in the specification describe abstract behavior without committing to a physical representation.

Ancestors (12)

  1. a
  2. 2
  3. Imperative programming
  4. 2013
  5. Past exam of the year 1 of the computer science course of the University of Oxford
  6. Year 1 of the computer science course of the University of Oxford
  7. Computer science course of the University of Oxford
  8. Undergraduate course of the University of Oxford
  9. Course of the University of Oxford
  10. University of Oxford
  11. List of universities
  12. Home

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version