VDM-SL cheatsheet [Definitions]

Toplevel definitions

Definitions in seach section of a flat specification or a module
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;

Local definitions

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]

Patterns

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

Bindings

type bind pattern:type
{mk_(b1, b2) | b1, b2:bool}
set bind pattern in set set expression {mk_(b1, b2) | b1, b2 in set {true, false}}