Based on appendix A in The Way of Z.

Links to more Z examples.

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

Other Z pages

Acknowledgements

## Names

a,bidentifiersd,edeclarations (e.g.,a: A; b, ...: B ...)f,gfunctionsm,nnumbersp,qpredicatess,tsequencesx,yexpressionsA,BsetsC,DbagsQ,RrelationsS,TschemasX,schema text (e.g.,dd | p, orS)## Definitions

a == xAbbreviation definitiona ::= b | ...Free type definition[a]Introduction of a given set (or[a,...])a _Prefix operator_ aPostfix operator_ a _Infix operator## Logic

trueLogical true constantfalseLogical false constantpLogical negation,notp qLogical conjunction,andp qLogical disjunction,orp qLogical implicationp qLogical equivalenceX qUniversal quantificationX qExistential quantification(leta == x; ... p)Local definition## Sets and expressions

x = yEqualityx yInequalityx ASet membershipx ANon-membershipEmpty setA BSet inclusionA BStrict set inclusion{ x, y, ... }Set display{ X x }Set comprehension( X x)Lambda expression(leta == x; ... y)Local definitionifpthenxelseyConditional expression(x,y, ...)Tuple(x,y)PairA B ...Cartesian productAPower setA BSet intersectionA BSet unionA \ BSet differencefirst xFirst element of an ordered pairsecond xSecond element of an ordered pair# ANumber of elements in a set## Relations

A BBinary relation ((A B))a bMaplet ((a,b))domRDomain of a relationranRRange of a relationQ RForward relational compositionQ RBackward relational composition (R Q)A RDomain restrictionA RDomain anti-restrictionA RRange restrictionA RRange anti-restrictionR ARelational imageR^{~}Inverse of relationR^{+}Transitive closureQ RRelational overridingaRbInfix relation## Functions

A BPartial functionsA BTotal functionsA BPartial injectionsA BTotal injectionsA BBijectionsf xFunction application (orf(x))## Numbers

Set of integersSet of natural numbers{ 0, 1, 2, ... }_{1}Set of strictly positive numbers{ 1, 2, ... }m+nAdditionm-nSubtractionm*nMultiplicationmdivnDivisionmmodnRemainder (modulus)m nLess than or equalm < nLess thanm nGreater than or equalm > nGreater thanm .. nNumber rangemin AMinimum of a set of numbersmax AMaximum of a set of numbers## Sequences

seq ASet of finite sequencesseq_{1}ASet of non-empty finite sequencesiseq ASet of finite injective sequencesEmpty sequencex, y, ...Sequence displays tSequence concatenationhead sFirst element of a sequencetail sAll but the head element of a sequencelast sLast element of a sequencefront sAll but the last element of a sequencesintSequence segment relation## Axiomatic definition

d p ## Schema

S d p ## Generic Definition

[a, ...] d p ## Schema Calculus

S [ X ]Horizontal schema[ T; ... | ... ]Schema inclusionz.aComponent selection (givenz:S)SBindingSSchema negationS TSchema conjunctionS TSchema disjunctionS TSchema compositionS >> TSchema piping## Conventions

a?Input to an operationa!Output from an operationaState component before an operationa'State component after an operationSState schema before an operationS'State schema after an operationSChange of stateSNo change of state

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.

Z home page with FAQ and links to publications, tools, and meetings.

Back to top

Jonathan Jacky / Department of Radiation Oncology Box 356043

University of Washington / Seattle, Washington 98195-6043 / USA

Tel (206) 598-4117 / Fax (206) 598-6218

E-mail: jon@u.washington.edu