Blocks
sequential execution of multiple statements
| block statement |
(statement;
...;
statement)
(dcl name:type:=expression,...;
statement;
...;
statement)
|
(dcl tmp:nat := v1;
v1 := v2;
v2 := tmp)
|
Skip
do nothing
| skip statement |
skip |
skip
while do_something_and_may_return_false_to_terminate() do skip
|
Assignments
| assignment statement |
lefthand := expression |
x := x + 1
p.x := p.x + 1
ps(3).x := ps(2).x + 1
|
| atomic statement |
atomic(assignment;...;assignment) |
atomic(x := x + 1; y := y - 1) |
lefthandside
| variable name |
name |
x := x + 1 |
| field reference |
lefthand.name |
p.x := p.x + 1
ps(3).x := ps(2).x + 1
|
| application reference |
lefthand(expression) |
ps(3) := ps(2)
car.wheels(3) := wheel
|
Operation calls
subroutine call controls
| call statement |
name(expression,...,expression) |
inc()
add(2)
|
| return statement |
return
return expression
|
return
return x + y
|
Branches
| if statement |
if conditional expression then statement else statement
if conditional expression then statement
elseif conditional expression then statement
...
else statement
|
if 3 mod 2 = 0 then return <even> else return <odd>
if 10 mod 15 = 0 then return <FizzBuzz>
elseif 10 mod 5 = 0 then return <Buzz>
elseif 10 mod 3 = 0 then return <Fizz>
else return 10
|
| cases statement |
cases expression:
pattern,..,pattern -> statement,
...,
pattern,...,pattern -> statement,
others -> statement
end
|
cases mk_('+', 1, 2):
mk_('+', x, y) -> return x + y,
mk_('-', x, y) -> return x - y,
others -> return <ERROR>
end
cases "03-123-4567":
city^"-"^area^"-"^local -> return mk_(city, area, local),
others -> return <ERROR>
end
|
Loops
| while loop |
while conditional expression do statement
|
while not finished() do something()
|
| 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]
|
Local definitions
| 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 return f(2)
|
| let be statement |
let multiple bind be st conditional expression in expression
|
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)
|