- Binary Search:
The following is an implementation of
binary search on an integer array in Xanadu. The novelty in
the implemenation is the annotation following the keyword
invariant. This annotation is a dependent type that
asserts some information at the entrance point of the loop. In
this case, the annotation states that variables low
and high have types int(i) and
int(j) at the loop entrance point for some integers
i and j such that both 0 <= i <= n
and 0 <= j+1 <= n hold. This is a loop invariant,
which can guarantee the array subscripting operation
vec[mid] in the body of the loop is safe, that is, it
can never go out of bounds. The crucial point is that
type-checking in Xanadu can automatically verify whether a
program invariant like this, which is provided by the
programmer, is indeed a correct program invariant.
In addition, it is also automatically checked in Xanadu
whether a variable is already initialized before it is read.
{n:nat}
int bsearch(key: int, vec[n]: int) {
var: int low, mid, high;
int x;;
low = 0; high = arraysize(vec) - 1;
invariant:
[i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
while (low <= high) {
mid = (low + high) / 2;
x = vec[mid];
if (key == x) { return mid; }
else if (key < x) { high = mid - 1; }
else { low = mid + 1; }
}
return -1;
}
- List Reverse:
This example demonstrates that it can be verified in the
type system of Xanadu that a list reverse function is length preserving.
The following declaration declares a polymorphic union type
<'a> list. The two constructors Nil and
cons associated with the union type are given types
<'a> list(0) and {n:nat} 'a * <'a> list(n) ->
<'a> list(n+1), respectively, meaning that Nil
is a list of length 0 and Cons returns a
list of length n+! when given an element and a list
of length n. Note that {n:nat} indicates
that n, an type index variable of sort nat,
is universally quantified. nat is the sort for a type
index that represents a natural number.
union <'a> list with nat {
Nil(0);
{n:nat} Cons(n+1) of 'a * <'a> list(n)
}
The following implements the reverse append function on lists.
The header of the function states that for natural numbers
m and n, rev_app takes a pair of
lists of lengths m and n and returns a list
of length m+n. It is clear that exit,
meaning that a program halts abnormally, can never be execute
at run-time and therefore unnecessary in the case. Unfortunately,
this information can not be captured in the type system of Xanadu.
('a){m:nat, n:nat}
<'a> list(m+n) rev_app
(xs: <'a> list(m), ys: <'a> list(n)) {
var: 'a x;;
invariant:
[m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1))
while (true) {
switch (xs) {
case Nil: return ys;
case Cons(x, xs): ys = Cons(x, ys);
}
}
exit;
}
The list reverse function can now be implemented as
follows. The header of the function indicates that this is a
length preserving function.
('a){n:nat}
<'a> list(n) reverse (xs: <'a> list(n)) {
return rev_app (xs, Nil);
}
- Sparse Array Multiplication:
We implement the multiplication between a sparse array and a
vector. We define a polymorphic record
<'a>sparseArray for representing two dimensional
sparse arrays in which each element is of type
'a. <'a>sparseArray is indexed with a pair
of natural numbers (m,n), which stand for the
number of rows and the number of columns in a sparse array,
respectively. Let sa be a record of type <'a>
sparseArray(m, n). Then sa has three
components, namely, row, col and
data. Clearly, the types assigned to row
and col indicate that sa and
sa.col return the dimensions of sa The
type assigned to data states that sa.data
is an array of size m. In this array, each element,
which represents a row in a sparse array, is a list of pairs
and each pair consists of a natural number less than
n and an element of type 'a.
{m:nat,n:nat}
record <'a> sparseArray(m, n) {
row: int(m);
col: int(n);
data[m]: <int[0,n) * 'a> list
}
The function mat_vec_mult takes a float point sparse
array of dimension (m,n) and a float point vector of
size n and returns a float point vector of size
m. Note that the function list_vec_mult is
used for computing the dot product of a row in the sparse
array and the vector. The point we make is that the type
system of Xanadu can guarantee all array subscripting
operations in this example to be safe at run-time.
{n:nat}
float
list_vec_mult (xs: <int[0,n) * float> list, vec[n]: float) {
var: int i; float f, sum;;
sum = 0.0;
while (true) {
switch (xs) {
case Nil: return sum;
case Cons((i, f), xs): sum = sum +. f *. vec[i];
}
}
exit;
}
{m:nat,n:nat}
<float> array(m)
mat_vec_mult(mat: <float> sparseArray(m, n), vec[n]: float) {
var: nat i; float result[];;
result = newarray(mat.row, 0.0);
for (i = 0; i < mat.row; i = i + 1) {
result[i] = list_vec_mult (mat.data[i], vec);
}
return result;
}
- Heapsort:
Could you figure out this one by yourself :-)
{max:nat}
record <'a> heap(max) {
max: int(max);
mutable size: [size:nat | size <= max] int(size);
data[max]: 'a
}
{max:nat, i:nat | i < max}
unit heapify (heap: <float> heap(max), i: int(i)) {
var: int size, left, right;
float temp;
largest: [a:nat | a < max] int(a) ;;
left = 2 * i + 1; right = 2 * i + 2;
size = heap.size; largest = i;
if (left < size) {
if (heap.data[left] >. heap.data[i]) { largest = left; }
}
if (right < size) {
if (heap.data[right] >. heap.data[largest]) { largest = right; }
}
if (largest <> i) {
temp = heap.data[i];
heap.data[i] = heap.data[largest];
heap.data[largest] = temp;
heapify (heap, largest);
}
}
{max:nat}
unit buildheap (heap: <float> heap(max)) {
var: int i, size;;
size = heap.size;
invariant: [i:int | i < max] (i: int(i))
for (i = size / 2 - 1; i >= 0; i = i - 1) {
heapify (heap, i);
}
}
{max:nat}
unit heapsort (heap: <float> heap(max)) {
var: int size, i; float temp;;
buildheap (heap);
invariant: [i:int | i < max] (i: int(i))
for (i = heap.max - 1; i >= 1; i = i - 1) {
temp = heap.data[i];
heap.data[i] = heap.data[0];
heap.data[0] = temp;
heap.size = i;
heapify(heap, 0);
}
}
- Gaussian Elimination:
Could you figure out this one by yourself :-)
{m:nat, n:nat}
record <'a> matrix(m,n) {
row: int(m);
col: int(n);
data[m][n]: 'a
}
{m:nat,n:nat,i:nat,j:nat | i < m, j < m}
unit
rowSwap(data[m][n]: float, i:int(i), j:int(j)) {
var: temp[]: float;;
temp = data[i];
data[i] = data[j];
data[j] = temp;
}
{n:nat,i:nat | i < n}
unit
norm(r[n]: float, n:int(n), i:int(i)) {
var: float x;;
x = r[i]; r[i] = 1.0; i = i + 1;
invariant: [i:nat] (i: int(i))
while (i < n) { r[i] = r[i] /. x; i = i + 1;}
}
{n:nat, i:nat | i < n}
unit
rowElim(r[n]: float, s[n]: float, n:int(n), i: int(i)) {
var: float x;;
x = s[i]; s[i] = 0.0; i = i + 1;
invariant: [i:nat] (i: int(i))
while (i < n) { s[i] = s[i] -. x *. r[i]; i = i + 1;}
}
{m:nat, n:nat, i:nat | m > i, n > i}
[k:nat | k < m] int(k)
rowMax (data[m][n]: float, m: int(m), i: int(i)) {
var: nat j; float x, y;
max: [k: nat | k < m] int(k);;
max = i; x = fabs(data[i][i]); j = i + 1;
while (j < m) {
y = fabs(data[j][i]);
if (y >. x) { x = y; max = j; }
j = j + 1;
}
return max;
}
{n:nat | n > 0}
unit gauss (mat: <float> matrix(n,n+1)) {
var: float data[][n+1]; nat i, j, max, n;;
data = mat.data; n = mat.row;
for (i = 0; i < n; i = i + 1) {
max = rowMax(data, n, i);
norm (data[max], n+1, i);
rowSwap(data, i, max);
for (j = i + 1; j < n; j = j + 1) {
rowElim(data[i], data[j], n+1, i);
}
}
}
- More Examples:
Please find more and larger examples here.