Appendix C: Standard Library Data Types

Assumes: §1.6 (data types and match) and Part 3 (functors).

Besides the built-in types from §1.1, the standard library provides generic data types as functors in the module Library. This appendix describes the ones the main tutorial doesn't use: options, lists, sequences, and arrays.

C.1 Getting an instance

Each data type is a functor over Library.Type, the interface of all types, so you choose the element type by instantiating it. You can declare an instance explicitly, as in module IntOption = Library.Option[Int]. You can also write the instance as a type, as in List[Int], or let Raven infer it from a call (§3.6). Each instance's type is called T, and Library.Type also gives every element type an unspecified value default.

The names Option, List, Seq and Array are available in every program without an import, as if it started with import Library.Option and so on. A declaration of one of these names in your own program takes precedence.

C.2 Options

Library.Option[E] holds either no value or one value of type E:

rep type T = data {
  case none
  case some(value: E)
}

is_some(x) tests for the second case. The examples in this appendix's first file, options_and_lists.rav, include a function returning the first element of a list, if there is one:

func first(l: List[Int]) returns (r: IntOption.T) {
  l == nil ? IntOption.none : IntOption.some(l.hd)
}

To get at the value, write first(l).value. A destructor is looked up in the data type of the value it is applied to, so it needs no module name, as for l.hd here.

C.3 Lists

Library.List[E] is the familiar inductive list, built from nil and the infix constructor :: (with destructors hd and tl), together with recursive functions for length, membership, and concatenation: len(l), e in l, and l ++ tail. The prelude also provides literals <||>, <|1|>, and <|1, 2|>. An empty literal gets its element type from context, as in val xs: List[Int] := <||>;. After import List._, you can write lists as in 1 :: 2 :: nil and use the functions unqualified. Lists are ordinary data types, so you can define your own functions on them by recursion and match:

func sum(l: List[Int]) returns (r: Int)
  decreases l
{
  match l {
    case nil => 0
    case hd :: tl => hd + sum(tl)
  }
}

Raven unfolds the definitions of such functions automatically, so facts about concrete lists, such as sum(1 :: 2 :: nil) == 3, hold without further proof.

C.4 Sequences

Library.Seq[E] provides immutable sequences with the following operations, most of which can also be written with a notation of their own:

Operation	Notation	Meaning
empty, singleton(e)	[], [e]	the empty sequence, and the sequence holding just e
length(s)		the number of entries of s
index(s, i)	s[i]	the entry at position i, counting from 0
append(s, t)	s ++ t	s followed by t
update(s, i, e)	s[i := e]	s with the entry at position i replaced by e
take(s, n), drop(s, n)	s[..n], s[n..]	the first n entries of s, and the remaining ones
contains(s, e)	e in s	whether e is an entry of s
equal(s, t)	s == t	whether s and t have the same entries

index is unspecified outside the range from 0 to length(s) - 1. As with a map, the statement s[i] := e is short for s := s[i := e]. The slice s[m..n] holds the entries from position m up to, but excluding, position n, and is short for s[..n][m..].

You can write a sequence as a literal, listing its entries between [ and ], as in [1, 2, 3], much as you write a set as {1, 2, 3}. The empty sequence [], like Seq.empty, takes its instance from the type expected where it appears, as in s == [], or from an annotation, as in ([] : Seq[Int]).

Unlike List, Seq is sealed (§3.7). Its interface, Library.SeqSpec[E], states the properties of these operations as auto lemmas, and those lemmas are all you see as a client. Seq implements sequences as lists and proves the lemmas, but none of that is visible outside it.

hit_log.rav brings back the hit counter. This version keeps a log of its hits, each numbered when it happens, instead of a number:

module HitLog {
  module Log = Library.Seq[Int]

  field log: Log.T

  pred valid(c: Ref, v: Int) {
    exists l: Log.T :: own(c.log, l) && Log.length(l) == v &&
      (forall i: Int :: {l[i]} 0 <= i && i < v ==> l[i] == i)
  }

  proc increment(c: Ref, ghost v: Int)
    requires valid(c, v)
    ensures valid(c, v + 1)
  {
    unfold valid(c, v)
    var l := c.log
    c.log := l ++ [Log.length(l)]
    fold valid(c, v + 1)
  }

  // ... create and get
}

valid(c, v) says that the log of a counter with value v holds 0, 1, ..., v - 1. The proof of increment needs the length and the entries of the extended log, and SeqSpec's lemmas about append, singleton, length and index provide them without any help. The log itself appears as an existentially quantified l in valid, and Raven finds it when you fold valid (§E.3).

Two sequences with the same length and the same entries are equal, and Raven compares sequences entry by entry whenever it needs to decide whether they are equal. So the lemma split at the end of hit_log.rav needs no proof:

lemma split(s: Seq[Int], n: Int)
  requires 0 <= n && n <= Seq.length(s)
  ensures s[..n] ++ s[n..] == s
{}

Here, Seq[Int] names the sequences of integers, and each call such as Seq.length(s) infers the instance from the type of its argument (§3.6).

C.5 Arrays

Options, lists, and sequences are values. Library.Array[E] is different: an array is a family of heap cells, one per index, each holding an entry of type E in its field value:

Member	Meaning
length(a)	the number of cells of a
loc(a, i)	the cell at index i, a Ref
arr(a, m)	a predicate owning all cells of a, whose entries are given by the map m
alloc(n, d)	a procedure creating an array of n cells, each holding d

m is E.default outside the bounds of a, so the entries determine it. Distinct indices, and distinct arrays, have distinct cells. This is what lets an iterated separating conjunction like the one in arr own all of them at once (§5.3.2). A Ref can't be constructed in Raven, so this fact can't be proved. Like alloc, it is an axiom of the standard library, which you can rely on instead of stating it yourself.

You access entries by indexing, as with maps. x := a[i] reads the entry at index i, a[i] := v writes it, and own(a[i], v) owns it. These are short for x := loc(a, i).value, loc(a, i).value := v, and own(loc(a, i).value, v). The atomic operations of §4.1 work on entries too, as in faa(a[i], 1). Unlike a map lookup, though, a[i] is not an expression. Like a field, an entry can only be read by an assignment, as in x := a[i] or var x := a[i], or named as a location, as in own and the atomic operations. A trigger therefore mentions the cell, as in {loc(a, j)} below.

arrays.rav sets all entries of an array to the same value. It imports the members of Library.Array, so that arr, length and loc apply to an Array[Int] directly, with the instance inferred from the argument (§3.6):

proc fill(a: Array[Int], x: Int, implicit ghost m: Map[Int, Int])
  requires arr(a, m)
  ensures arr(a, { i: Int :: 0 <= i && i < length(a) ? x : m[i] })
{
  unfold arr(a, m);
  var i := 0;
  while (i < length(a))
    invariant 0 <= i && i <= length(a)
    invariant forall j: Int :: {loc(a, j)} 0 <= j && j < i ==> own(a[j], x)
    invariant forall j: Int :: {loc(a, j)} i <= j && j < length(a) ==> own(a[j], m[j])
  {
    a[i] := x;
    i := i + 1;
  }
  fold arr(a, { i: Int :: 0 <= i && i < length(a) ? x : m[i] });
}

Inside the loop, arr is unfolded, so the invariants own the cells individually: those already written hold x, the others still hold their entries from m. After the loop, folding arr again packs them up into a single predicate with the new entries.