Comments
// Single line comment
(* Multi-line
comment *)
Strings
"foo \"bar\" baz";
'foo \'bar\' baz';
Numbers
123
123.456
-123.456
1e-23
123.456E789
0xaf
0xAF
Functions
foo()
Bar()
_456()
Full Example
function pop (const h : heap) : (heap * heap_element * nat) is
begin
const result : heap_element = get_top (h) ;
var s : nat := size(h) ;
const last : heap_element = get_force(s, h) ;
remove s from map h ;
h[1n] := last ;
s := size(h) ;
var i : nat := 0n ;
var largest : nat := 1n ;
var left : nat := 0n ;
var right : nat := 0n ;
var c : nat := 0n ;
while (largest =/= i) block {
c := c + 1n ;
i := largest ;
left := 2n * i ;
right := left + 1n ;
if (left <= s) then begin
if (heap_element_lt(get_force(left , h) , get_force(i , h))) then begin
largest := left ;
const tmp : heap_element = get_force(i , h) ;
h[i] := get_force(left , h) ;
h[left] := tmp ;
end else skip ;
end else if (right <= s) then begin
if (heap_element_lt(get_force(right , h) , get_force(i , h))) then begin
largest := right ;
const tmp : heap_element = get_force(i , h) ;
h[i] := get_force(right , h) ;
h[left] := tmp ;
end else skip ;
end else skip ;
}
end with (h , result , c)