externally_immutable.rs

// This gives an example of a specification for an
// "interior mutability, externally pure" object

// Consider a doubly-linked list that internally uses Cell<Rc<T>> to implement
// its cyclic data structure. However, we don't want these implementation
// details to be visible externally. We don't even want the external specification
// to say that this object has a dependence on the heap, but we want to present
// a `view()` interpretation function that returns a sequence.
// This is how we can do it.

// Start with a Node type:

struct Node<T> {
  pub prev: Cell<Option<Rc<Node<T>>>>,
  pub next: Cell<Option<Rc<Node<T>>>>,
  pub value: T,
}

struct DoublyLinkedList<T> {
  head: Cell<Option<Rc<Node<T>>>,
  tail: Cell<Option<Rc<Node<T>>>,

  // A "Heap" is basically a map from Cell<X> to an X
  ghost cell_map: Heap,
}

impl<T> DoublyLinkedList<T> {
  #[spec]
  pub view(cell: &Cell<Option<Rc<Node<T>>>>, cell_map: Heap) -> seq<T>
  // ... requires some condition about cells actually being in the cell_map
  {
    // look up the contents of the cell from the fictional ghost heap
    let node_opt = cell_map[cell];

    // basic case analyis and recursion now
    match node_opt {
      None => [] // end of the list, return empty seq
      Some(node) => {
        return [node.value] + view(node.next)
      }
    }
  }

  #[spec]
  pub view(&self) -> seq<T> {
    // this function can be pure because `self` contains all the heap information
    // needed to compute the sequence
    node_tail(self.head, self.cell_map)
  }

  pub get_first(&self) -> (t: T)
  requires self.view().len() > 0
  ensures t == Some(self.view()[0])
  {
    // I'm assuming with this methodology that Cell::get is modified to take
    // a ghost heap as a parameter.
    // The specification of `cell.get(heap)` is that it returns `heap[cell]`.
    match self.head.get(&self.ghost_heap) {
      None => { assert!(false); }
      Some(node) => node.value
    }
  }
}