| section |
description |
syntax |
example |
types |
type alias |
name = type inv pattern == conditional expression;
|
pair = nat * nat;
pair = nat * nat inv mk_(x, y) == x + 1 = y;
pair = nat * nat inv p == p.#1 + 1 = p.#2;
|
| record definition |
name :: fieldname:type fieldname:type... inv pattern == conditional expression;
|
Point :: x:real y:real;
FirstQuadrant :: x:real y:real inv mk_FirstQuadrant(x, y) == x >= 0 and y >= 0;
FirstQuadrant :: x:real y:real inv p == p.x >= 0 and p.y >= 0;
|
values |
constant value definition |
name : type = expression;
|
PI : real = 3.141592653589793238
PI2 = PI * 2
|
functions |
explicit function definition |
name: type * ... * type -> type
name(pattern,...,pattern) == expression
pre conditional expression
post conditional expression
measure functionname
|
mid : real * real -> real
mid(x, y) == (x + y) / 2
pre x <= y
post x <= RESULT and RESULT <= y;
|
state |
state definition |
state statename of
name:type
name:type
...
inv pattern == conditional expression
init pattern == pattern = mk_statename(expression,...,expression)
end
|
state Cursor of
col : nat
row : nat
inv mk_Cursor(x, y) == x < 80 and y < 25
init s == s = mk_Cursor(0, 0)
end
|
operations |
pure operation definition |
pure name: type * ... * type ==> type
name(pattern,...,pattern) == statement
pre conditional expression
post conditional expression
|
pure cursorColumn: () ==> nat
cursorColumn() == return col
post RESULT = col;
|
| explicit operation definition |
name: type * ... * type ==> type
name(pattern,...,pattern) == statement
pre conditional expression
post conditional expression
|
moveColumn: int ==> ()
moveColumn(dx) == cur := cur + dx
pre
let x == cursorColumn() + dx
in (y >= 0 and y < 80)
post cur~ + x = cur;
|
| kind |
description |
syntax |
example |
| expression |
let expression |
let pattern:type=expression,...,pattern:type=expression in expression
|
let x:nat = 1 in x + 1
let x = 1 in x + 1
let x:nat = 1, y:nat = 2 in x + y
let f:nat -> nat1 f(x) == x + 1 in f(2)
|
| let be expression (conditional matching) |
let multiple bind be st conditional expression in expression
|
let x in set {1,2,3,4} be st x mod 2 = 0 in x
let b1, b2:bool be st b1 => b2 in mk_(b1, b2)
|
| statement |
let statement |
let pattern:type=expression,...,pattern:type=expression in statement
|
let x:nat = 1 in return x + 1
let x = 1 in return := x + 1
let x:nat = 1, y:nat = 2 in return x + y
let f:nat -> nat1 f(x) == x + 1 in f(2)
|
| let be statement (conditional matching) |
let multiple bind be st conditional expression in statement
|
let x in set {1,2,3,4} be st x mod 2 = 0 in return x
let b1, b2:bool be st b1 => b2 in return mk_(b1, b2)
|
| block variable |
(dcl name:type=expression,...,name:type=expression; statement; ...)
|
(dcl tmp:nat := v1; v1 := v2; v2 := tmp)
|
| int for loop |
for name = integer expression to integer expression by integer expression do statement
|
for i = 1 to 10 do s := s ^ [i]
|
| sequance for loop |
for pattern in sequence expression do statement
|
for i in [1,2,3,4,5] do s := s ^ [i]
|
| set for loop |
for all pattern in set set expression do statement
|
for all i in set {1,...,10} do s := s ^ [i]
|
| type |
description |
syntax |
example |
| any |
identifier |
name |
let x = 1 in x + 2
|
| don't care |
- |
let - = 1 in 2
|
| value |
literal
(expression)
|
cases 4 mod 2: 0 -> <odd>, 1 -> <even> end
|
| product |
tuple pattern |
mk_(pattern,...,pattern) |
let mk_(x, y) = mk_(1, 2) in x + y
|
| record |
record pattern |
mk_name(pattern,...,pattern) |
let mk_Point(x, y) = mk_Point(1, 2) in x + y
|
| set |
set enumeration pattern |
{pattern,...,pattern} |
let {x, y} = {1, 2} in x + y
|
| set union pattern |
pattern union pattern |
let {x} union {1, 3} = {1, 2, 3} in x
|
| seq |
sequence enumeration pattern |
[pattern,...,pattern] |
let [x, y] = [1, 2] in x + y
|
| concat pattern |
pattern ^ pattern |
let x^[3] = [1,2,3] in x
|
| map |
map enumeration pattern |
[pattern |-> pattern,...,pattern |-> pattern] |
let {2 |-> -, 1 |-> x} = {1 |-> 2, 2 |-> 3} in x
|
| map union pattern |
pattern munion pattern |
let - munion {1 |-> x} = {1 |-> 2, 2 |-> 3} in x
|