Chapter 14. Dataviews as Linear Dataprops

Table of Contents
Optional Views
Disjunctive Views
Dataview for Linear Arrays
Dataview for Linear Strings
Dataview for Singly-Linked Lists
Proof Functions for View-Changes

The at-views of the form T@L for types T and addresses L are building blocks for constructing other forms of views. One mechanism for putting together such building blocks is by declaring dataviews, which is mostly identical to declaring dataprops. I now present in this chapter some commonly encountered dataviews and their uses.

Please find on-line the code presented for illustration in this chapter.

Optional Views

The dataview option_v is declared as follows:

dataview option_v (v:view+, bool) = | Some_v (v, true) of (v) | None_v (v, false) of ()

This declaration indicates that the dataview option_v is covariant in its first argument and there are two proof constructors associated with it: Some_v and None_v. Given a view V, option_v(V, b) is often called an optional view, where b is a boolean. Clearly, a proof of the view option_v(V, true) contains a proof of the view V while a proof the view option_v(V, false) contains nothing.

As an example, the following function interface involves a typical use of optional view:

fun{a:t@ype} ptr_alloc_opt (): [l:addr] (option_v (a? @ l, l > null) | ptr l)

Given a type T, the function ptr_alloc_opt<T> returns a pointer paired with a proof of an optional view; if the returned pointer is not null, then the proof can be turned into a proof of the view T?@L, where L is the location to which the pointer points; otherwise, there is no at-view associated with the returned pointer.