union <'a> list with nat { Nil(0); {n:nat} Cons(n+1) of 'a * <'a> list(n) } {n:nat} float list_vec_mult (xs: <[i:int | 0 <= i < n] (int(i) * float)> list, vec[n]: float) { var: int i; float f, sum;; sum = 0.0; invariant: (xs: <[i:int | 0 <= i < n] (int(i) * float)> list) while (true) { switch (xs) { case Nil: return sum; case Cons((i, f), xs): sum = sum +. f *. vec[i]; } } exit; } /* union natural with nat { Z(0); {a:nat} S(a+1) of natural(a) } global x: int = 0 unit inc () { x = x + 1; } {m:nat,n:nat} int(min(m,n)) min(x:natural(m), y:natural(n)) { switch (x, y) { case (S(x), S(y)): return 1+min(x,y); } } ('a){m:nat,n:nat} <'a> list(m+n) append (xs: <'a> list(m), ys: <'a> list(n)) { var: 'a x;; switch (xs) { case Nil: return ys; case Cons(x, xs): return Cons(x, append(xs, ys)); } } ('a){n:nat} [i:nat] <'a> list(i) flatten (xss: <[i:nat] <'a> list(i)> list(n)) { var: <'a> list xs, ys;; switch (xss) { case Nil: return Nil; case Cons(xs, xss): ys = flatten (xss); return append(xs, ys); } } ('a,'b){n:nat} <'a> list(n) * <'b> list(n) split (xs: <'a * 'b> list(n)) { var: 'a y; 'b z; <'a> list ys; <'b> list zs;; switch (xs) { case Cons((y, z), xs): switch (split(xs)) { case (ys, zs): return(Cons(y, ys), Cons(z, zs)); } } } ('a){m:nat,n:nat | n < m} 'a nth (xs: <'a> list(m), n: int(n)) { var: 'a x; int y;; y = n; invariant: [m:nat, n:nat | n < m] (xs: <'a> list(m), y: int(n)) while (true) { switch (xs) { case Cons(x, xs): if (y == 0) return x; } } exit (1); } [n: int | n >= 0] int(n) foo () { var: int i;; i = -100; while (i < 0) { i = i + 1; } return i; } unit foo () { var: int n, n4, i0, i1, i2, i3;; i0 = 0; i1 = 0; i2 = 0; i3 = 0; n = 16; n4 = 4; invariant: [i0:nat,i1:nat,i2:nat,i3:nat | i0 <= i1 <= i2 <= i3] (i0: int(i0), i1: int(i1), i2: int(i2), i3: int(i3)) while (i3 <= n) { i0 = i0 + n4; i1 = i1 + n4; i2 = i2 + n4; i3 = i3 + n4; } } int foo () { var: [n:nat] int(n) i;; i = 0; while (true) { i = i + 1; } i = i; return i; } int int_add (x: int, y: int) { return x + y ; } {a:nat} [m:int | m < a] int(m) foo (x: int(a)) { return (x - 1); } {b:nat} [n:int | n < b] int(n) bar (x: int(b)) { return foo (x); } {size:nat, i:nat, j:nat, k:nat | i < size, j < size, k < size} [n:nat | n < size] int(n) median(i:int(i), j:int(j), k:int(k), vec[size]: float) { var: float x, y, z;; x = vec[i]; y = vec[j]; z = vec[k]; if (x >. y) { if (y >. z) return j; else { if (x >. z) return k; else return i; } } else { if (y >. z) { if (x >. z) return i; else return k; } else return j; } } {size:nat, start:nat, end:nat | start < end <= size} [n:nat | n < size] int(n) get_pivot (start: int(start), end: int(end), vec[size]: float) { var: int diff, d; int i, j, k;; diff = end - start; if (diff < 7) return start + (diff / 2); else { i = start; j = start + diff / 2; k = end - 1; if (diff < 40) return median(i, j, k, vec); else { d = diff / 8; i = median(i, i + d, i + 2 * d, vec); j = median(j - d, j, j + d, vec); k = median(k - 2 * d, k - d, k, vec); return median(i, j, k, vec); } } } {size:nat, start: nat, end: nat | start < end <= size} [n:nat | start <= n < end] int(n) split(start: int(start), end: int(end), vec[size]: float) { var: int pivot; float x, temp; l: [i:int | start <= i <= end] int(i); h: [j:int | start <= j < end] int(j);; pivot = get_pivot(start, end, vec); l = start; h = end - 1; x = vec[pivot]; while (true) { while (l < end) { if (vec[l] <=. x) l = l + 1; else break; } while (start < h) { if (vec[h] >. x) h = h - 1; else break; } if (l < h) { temp = vec[l]; vec[l] = vec[h]; vec[h] = temp; l = l + 1; h = h - 1; } else return h; } } */