# Glossary of Z notation

Based on appendix A in The Way of Z.

This page looks best when this and this X are about the same size: X. See these viewing tips.

Names
Definitions
Logic
Sets and expressions
Relations
Functions
Numbers
Sequences
Axiomatic definition
Schema
Generic Definition
Schema Calculus
Conventions

#### Names

 a,b identifiers d,e declarations (e.g., a: A; b, ...: B ...) f,g functions m,n numbers p,q predicates s,t sequences x,y expressions A,B sets C,D bags Q,R relations S,T schemas X schema text (e.g., d, d | p, or S)

#### Definitions

 a == x Abbreviation definition a ::= b | ... Free type definition [a] Introduction of a given set (or [a,...]) a _ Prefix operator _ a Postfix operator _ a _ Infix operator

#### Logic

 true Logical true constant false Logical false constant p Logical negation, not p q Logical conjunction, and p q Logical disjunction, or p q Logical implication p q Logical equivalence X q Universal quantification X q Existential quantification (let a == x; ... p) Local definition

#### Sets and expressions

 x = y Equality x y Inequality x A Set membership x A Non-membership Empty set A B Set inclusion A B Strict set inclusion { x, y, ... } Set display {  X x  } Set comprehension ( X x) Lambda expression (let a == x; ... y) Local definition if p then x else y Conditional expression (x,y, ...) Tuple (x,y) Pair A B ... Cartesian product A Power set A B Set intersection A B Set union A \ B Set difference first x First element of an ordered pair second x Second element of an ordered pair # A Number of elements in a set

#### Relations

 A B Binary relation ( (A B)) a b Maplet ((a,b)) dom R Domain of a relation ran R Range of a relation Q R Forward relational composition Q R Backward relational composition (R Q) A R Domain restriction A R Domain anti-restriction A R Range restriction A R Range anti-restriction R A Relational image R ~ Inverse of relation R + Transitive closure Q R Relational overriding a R b Infix relation

#### Functions

 A B Partial functions A B Total functions A B Partial injections A B Total injections A B Bijections f x Function application (or f(x))

#### Numbers

 Set of integers Set of natural numbers { 0, 1, 2, ... } 1 Set of strictly positive numbers { 1, 2, ... } m+n Addition m-n Subtraction m*n Multiplication m div n Division m mod n Remainder (modulus) m n Less than or equal m < n Less than m n Greater than or equal m > n Greater than m .. n Number range min A Minimum of a set of numbers max A Maximum of a set of numbers

#### Sequences

 seq A Set of finite sequences seq1 A Set of non-empty finite sequences iseq A Set of finite injective sequences Empty sequence x, y, ... Sequence display s t Sequence concatenation head s First element of a sequence tail s All but the head element of a sequence last s Last element of a sequence front s All but the last element of a sequence s in t Sequence segment relation

 d p

 S d p

#### Generic Definition

 [a, ...] d p

#### Schema Calculus

 S [  X  ] Horizontal schema [  T; ... | ...  ] Schema inclusion z.a Component selection (given z:S) S Binding S Schema negation S T Schema conjunction S T Schema disjunction S T Schema composition S >> T Schema piping

#### Conventions

 a? Input to an operation a! Output from an operation a State component before an operation a' State component after an operation S State schema before an operation S' State schema after an operation S Change of state S No change of state

#### Other Z pages

Z mathematical tool-kit defines the operators shown in this glossary.

Z examples in web pages.

Z2HTML tool for translating LaTeX documents with Z markup to HTML web pages.