Editing Z notation (section)

==Usage and notation==
Z is based on the standard mathematical notation used in [[axiomatic set theory]], [[lambda calculus]], and [[first-order predicate logic]].<ref>{{cite book| last=Spivey | first=J. Michael | authorlink=Michael Spivey | title=The Z Notation: A Reference Manual | edition=2nd | location=Hemel Hempstead | publisher=[[Prentice Hall]] | series=International Series in Computer Science | date=1992 | isbn=978-0139785290 }}</ref> All expressions in Z notation are [[Type (model theory)|typed]], thereby avoiding some of the [[Naive set theory#Paradoxes|paradoxes of naive set theory]]. Z contains a standardized catalogue (called the ''mathematical toolkit'') of commonly used mathematical functions and predicates, defined using Z itself. It is augmented with '''Z schema''' boxes, which can be combined using their own operators, based on standard logical operators, and also by including schemas within other schemas. This allows Z specifications to be built up into large specifications in a convenient manner.

Because Z notation uses many non-[[ASCII]] symbols, the specification includes suggestions for rendering the Z notation symbols in [[ASCII]] and in [[LaTeX]]. There are also [[Unicode]] encodings for all standard Z symbols.<ref>{{cite web| url=https://unicode-search.net/unicode-namesearch.pl?term=Z%20NOTATION | title=Unicode Explained: Internationalize Documents, Programs, and Web Sites | first=Jukka K. | last=Korpela | website=unicode-search.net | access-date=24 March 2020 }}</ref>