VDM-SL cheatsheet [Expressions]

Local definitions

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)

Branchings

if expression if conditional expression then expression else expression
if conditional expression then expression elseif conditional expression then expression ... else expression
 if 3 mod 2 = 0 then <even> else <odd>
if 10 mod 15 = 0 then <FizzBuzz> elseif 10 mod 5 = 0 then <Buzz> elseif 10 mod 3 = 0 then <Fizz> else 10
cases expression cases expression: pattern,..,pattern -> expression,...,pattern,...,pattern -> expression, others -> expression end
 cases mk_('+', 1, 2):
  mk_('+', x, y) -> x + y,
  mk_('-', x, y) -> x - y,
  others -> <ERROR>
end
cases "03-123-4567":
  city^"-"^area^"-"^local -> mk_(city, area, local),
  others -> <ERROR>
end

Comparisons

Note: the types before and after = and <> must agree.
equality = ? * ? -> bool 1 = 1
1 = 2
1 = '1'
'1' = '1'
1 = 1.0
inequality <> ? * ? -> bool 1 <> 1
1 <> 2
1 <> '1'
'1' <> '2'
1 <> 1.0
＞ > real * real -> bool 1 > 1
2 > 1
≧ >= real * real -> bool 1 >= 1
1 >= 2
＜ < real * real -> bool 1 < 1
1 < 2
≦ <= real * real -> bool 1 <= 1
2 <= 1

Numerical expressions

addition + real * real -> real 1 + 2
subtraction - real * real -> real 1 - 2
multiplication * real * real -> real 1 * 2
division / real * real -> real 1 / 2
1 / 0
power ** real * real -> real 2 ** 3
quotient + int * int -> int 1 div 2
1 div 0
modulo mod int * int -> int 1 mod 2
-1 mod 2
1 mod -2
1 mod 0
remainder rem int * int -> int 1 rem 2
-1 rem 2
1 rem -2
1 rem 0
absolute value abs real -> real abs 2
abs -1
negation - real -> real - 3.14
-(2 + 3)
floor floor real -> int floor 3.14
floor -3.14

Boolean expressions

negation not bool -> bool not true
not false
conjunction and bool * bool -> bool true and true
true and false
true and undefined
false and undefined
undefined and false
disjunction or bool * bool -> bool false or false
true or false
true or undefined
false or undefined
undefined or true
implication => bool * bool -> bool true => true
true => false
false => false
false => undefined
undefined => true
equivalence <=> bool * bool -> bool true <=> true
false <=> false
true <=> false
inequivalence(exclusive or, xor) <> bool * bool -> bool true <> true
true <> false

Element access

tuple tuple expression.#nat literal mk_(1, 'a', 3).#1
mk_(1, 'a', 3).#2
mk_(1, 'a', 3).#3
record record expression.fieldname mk_Point(1,2).x
mk_Point(1,2).y

Applications

sequence sequence expression(nat expression) [0,2,4](2)
[0,2,4](10)
map map expression(expression) {0 |-> false, 1 |-> true}(0)
function (including lambda) function expression(expression,expression,...,expression) (lambda x:nat & x + 1)(2)
operation operation()
operation(expression,expression,...,expression)
 inc()
add(2)

Constructors

tuple mk_(expression,expression,...,expression) mk_(1,2,3)
mk_("abc", nil, 1)
token mk_token(expression) mk_token(1)
mk_token("abc")
mk_token(nil)
record mk_name(expression,expression,...,expression) mk_Point(1, 2.3)

Enumeration

set {}
{expression,expression,...,expression} 		{}
{1,2,3}
{1,2,{'3', nil}}
{1,...,10}
sequence []
[expression,expression,...,expression]
"Strings"
 []
[1,2,3]
[1,2,['3', nil]]
"Strings"
"Str" = ['S', 't', 'r']
map {|->}
{expression |->expression ,expression |-> expression,...,expression |-> expression} 		{|->}
{<apple> |-> 100, <orange> |-> 200, <cherry> |-> 150}

Comprehensions

set {x * 2 | x in set {1, ... ,5}}
{x * 2 | x in set {1, ... ,5} & x mod 2 = 0}
{mk_(b1, b2, b1 and b2) | b1,b2 : bool}
sequence [x * 2 | x in set {1, ... ,5}]
[x * 2 | x in set {1, ... ,5} & x mod 2 = 0]
map {"0123456789"(i+1) |-> i | i in set {0,...,9}}
{"0123456789"(i+1) |-> i | i in set {0,...,9} & i mod 2 = 0}

Set operators

membership in set T * set of T -> bool 1 in set {1,2,3}
0 in set {1,2,3}
{1,2} in set {0, {1, 2}, 3}
non membership not in set T * set of T -> bool 1 not in set {1,2,3}
0 not in set {1,2,3}
{1,2} not in set {0, {1, 2}, 3}
subset subset set of T * set of T -> bool {1,2} subset {1,2,3}
{1,2,3} subset {1,2,3}
{1,2,3} subset {1,2}
proper subset psubset set of T * set of T -> bool {1,2} psubset {1,2,3}
{1,2,3} psubset {1,2,3}
{1,2,3} psubset {1,2}
union union set of T * set of T -> set of T {1,2} union {2,3}
intersection inter set of T * set of T -> set of T {1,2} inter {2,3}
difference \ set of T * set of T -> set of T {1,2} \ {2,3}
cardinality (number of elements) card set of T -> nat card {1,...,10}
card {1, 2, nil}
card {}
distributed union dunion set of set of T -> set of T dunion {{1,2}, {2,3}}
dunion {{{1},2}, {2,3}}
distributed intersection dinter set of set of T -> set of T dinter {{1,2}, {2,3}}
dinter {{1,2, {3}}, {2,3}}
power set power set of T -> set of set of T power {1,2,3}
power {}

Sequence operators

slice ( ,..., ) seq of T * nat1 * nat1 -> T "Strings"(4,...,5)]
"Strings"(5,...,4)]
"Strings"(4,...,10)]
head element hd seq1 of T -> T hd [1,2,3]
hd "Strings"
tail element tl seq1 of T -> seq of T tl [1,2,3]
tl "Strings"
length len seq of T -> nat len [1,2,3,4,5]
len "Strings"
elements elems seq of T -> set of T elems [1,2,3,4,5]
elems "Strings"
indices inds seq of T -> set of nat1 inds [0,2,4]
inds "Strings"
reverse reverse seq of T -> seq of T reverse [0,2,4]
reverse "Strings"
concatenation ^ seq of T * seq of T -> seq of T [0,2,4]^[1,3,5]
"Str"^"ings"
distributed concatenation conc seq of seq of T -> seq of T conc [[0,2,4],[1,3,5]]
conc ["Str","ings"]
overridng ++ seq of T * map nat1 to T -> seq of T [0,2,4]++{2|->10}
"Your"++{1|->'H'}]

Map operators

domain dom map T1 to T2 -> set of T1 dom {0 |-> false, 1 |-> true}
range rng map T1 to T2 -> set of T2 rng {0 |-> false, 1 |-> true}
union munion map T1 to T2 * map T1 to T2 -> map T1 to T2 {0 |-> false, 1 |-> true} munion {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} munion {1 |-> true, 2 |-> false}
{0 |-> false, 1 |-> true} munion {1 |-> false, 2 |-> false}
overriding ++ map T1 to T2 * map T1 to T2 -> map T1 to T2 {0 |-> false, 1 |-> true} ++ {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} ++ {1 |-> false, 2 |-> false}
distributed union merge set of map T1 to T2 -> map T1 to T2 merge {{0 |-> false, 1 |-> true}, {2 |-> false, 3 |-> true}}
merge {{0 |-> false, 1 |-> true}, {1 |-> false, 2 |-> false}}
domain restriction <: set of T1 * map T1 to T2 -> map T1 to T2 {2,3} <: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
domain exclusion <-: set of T1 * map T1 to T2 -> map T1 to T2 {2,3} <-: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
range restriction :> map T1 to T2 * set of T2 -> map T1 to T2 {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :> {true, nil}
range exclusion :-> map T1 to T2 * set of T2 -> map T1 to T2 {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :-> {true, nil}
composition comp map T2 to T3 * map T1 to T2 -> map T1 to T3 {true|-><odd>, false|-><even>} comp {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
iteration ** map T1 to T1 * nat -> map T1 to T1 {0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 1
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 2
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 3
inverse inverse inmap T1 to T2 -> inmap T2 to T1 inverse {0 |-> '0', 1 |-> '1', 2 |-> '2'}

Quantifications

Universal quantifier forall multiple bind,...,multiple bind & expression forall i in set {1,2,3} & i mod 4 <> 0
forall i in set {1,2,3} & i mod 2 <> 0
forall b1,b2:bool & b1 or b2
Existential quantifier exists multiple bind,...,multiple bind & expression exists i in set {1,2,3} & i mod 4 = 0
exists i in set {1,2,3} & i mod 2 = 0
exists b1,b2:bool & b1 and b2
Unique existential quantifier exists1 bind & expression exists1 i in set {1,2,3} & i mod 2 = 0
exists1 i in set {1,2,3} & i mod 2 <> 0
exists1 mk_(b1,b2):bool*bool & b1 and b2

Iota

iota expression iota bind & expression iota i in set {1,2,3} & i mod 2 = 0
iota i in set {1,2,3} & i mod 4 = 0
iota i in set {1,2,3} & i mod 2 = 1

Lambda

lambda expression lambda name:type,...,name:type & expression (lambda x:real, y:real & x + y)(1,2)
(lambda x:real & lambda y:real & x + y)(1)(2)

Type discriminations

general is expression is_(expression, type) is_(10, nat1)
is_(3.14, nat1)
is_(10, real)
is_({1,...,10}, set of nat1)
primitive type is expression is_type(expression) is_nat1(10+20)
is_nat1(3.14)
is_real(10)
is_token(mk_token("abc"^"xyz"))

Undefined

undefined expression undefined undefined
nil = undefined
{1,2,undefined}
{1,2} union undefined