Z notation

The Z notation /ˈzɛd/ is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.

Agendacumple en Z
An example of a formal specification (in Spanish) using the Z notation.

History

In 1974, Jean-Raymond Abrial published "Data Semantics".[1] He used a notation that would later be taught in the University of Grenoble until the end of the 1980s. While at EDF (Électricité de France), Abrial wrote internal notes on Z. The Z notation is used in the 1980 book Méthodes de programmation.[2]

Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer.[3] It was developed further at the Programming Research Group at Oxford University, where Abrial worked in the early 1980s, having arrived at Oxford in September 1979.

Abrial has said that Z is so named "Because it is the ultimate language!"[4] although the name "Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory.

Usage and notation

Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic. All expressions in Z notation are typed, thereby avoiding some of the 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.

Although Z notation (just like the APL language, long before it) 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.

Standards

ISO completed a Z standardization effort in 2002. This standard[5] and a technical corrigendum[6] are available from ISO for free:

  • the standard is publicly available[5] from the ISO ITTF site free of charge and, separately, available for purchase[5] from the ISO site;
  • the technical corrigendum is available[6] from the ISO site free of charge.

See also

References

  1. ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L., Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
  2. ^ Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (in French), Eyrolles
  3. ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M., On the Construction of Programs, Cambridge University Press, ISBN 0-521-23090-X (describes early version of the language).
  4. ^ Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.
  5. ^ a b c "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 2002-07-01. 196 pp.
  6. ^ a b "ISO/IEC 13568:2002/Cor.1:2007". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1 (PDF). ISO. 2007-07-15. 12 pp.

Further reading

  • Spivey, John Michael (1992). The Z Notation: A reference manual. International Series in Computer Science (2nd ed.). Prentice Hall.
  • Davies, Jim; Woodcock, Jim (1996). Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall. ISBN 0-13-948472-8.
  • Bowen, Jonathan (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press. ISBN 1-85032-230-9.
  • Jacky, Jonathan (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge University Press. ISBN 0-521-55976-6.
Alkene

In organic chemistry, an alkene is an unsaturated hydrocarbon that contains at least one carbon–carbon double bond. The words alkene and olefin are often used interchangeably (see nomenclature section below). Acyclic alkenes, with only one double bond and no other functional groups, known as mono-enes, form a homologous series of hydrocarbons with the general formula CnH2n. Alkenes have two hydrogen atoms fewer than the corresponding alkane (with the same number of carbon atoms). The simplest alkene, ethylene (C2H4), with the International Union of Pure and Applied Chemistry (IUPAC) name ethene, is the organic compound produced on the largest scale industrially. Aromatic compounds are often drawn as cyclic alkenes, but their structure and properties are different and they are not considered to be alkenes.

Alloy (specification language)

In computer science and software engineering, Alloy is a declarative specification language for expressing complex structural constraints and behavior in a software system. Alloy provides a simple structural modeling tool based on first-order logic. Alloy is targeted at the creation of micro-models that can then be automatically checked for correctness. Alloy specifications can be checked using the alloy analyzer.

Although Alloy is designed with automatic analysis in mind, Alloy differs from many specification languages designed for model-checking in that it permits the definition of infinite models. The Alloy Analyzer is designed to perform finite scope checks even on infinite models.

The Alloy language and analyzer are developed by a team led by Daniel Jackson at the Massachusetts Institute of Technology in the United States.

CICS

Customer Information Control System (CICS) is a family of mixed language application servers that provide online transaction management and connectivity for applications on IBM mainframe systems under z/OS and z/VSE.

CICS is middleware designed to support rapid, high-volume online transaction processing. A CICS transaction is a unit of processing initiated by a single request that may affect one or more objects. This processing is usually interactive (screen-oriented), but background transactions are possible.

CICS provides services that extend or replace the functions of the operating system and are more efficient than the generalized services in the operating system and simpler for programmers to use, particularly with respect to communication with diverse terminal devices.

Applications developed for CICS may be written in a variety of programming languages and use CICS-supplied language extensions to interact with resources such as files, database connections, terminals, or to invoke functions such as web services. CICS manages the entire transaction such that if for any reason a part of the transaction fails all recoverable changes can be backed out.

While CICS has its highest profile among financial institutions such as banks and insurance companies, many Fortune 500 companies are reported to run CICS along with many government entities. CICS is also widely used by many smaller organizations. CICS is used in bank-teller applications, ATM systems, industrial production control systems, insurance applications, and many other types of interactive applications.

Recent CICS Transaction Server enhancements include support for Web services and Java, event processing, Atom feeds, and RESTful interfaces. CICS Transaction Server 5.5, which generally became available on December 14, 2018, reinforced CICS reputation as a mixed language application server, with the introduction of Node.JS support as well as new and enhanced capabilities in security, resilience and system management.

Cartesian product

In set theory (and, usually, in other parts of mathematics), a Cartesian product is a mathematical operation that returns a set (or product set or simply product) from multiple sets. That is, for sets A and B, the Cartesian product A × B is the set of all ordered pairs (a, b) where aA and bB. Products can be specified using set-builder notation, e.g.

A table can be created by taking the Cartesian product of a set of rows and a set of columns. If the Cartesian product rows × columns is taken, the cells of the table contain ordered pairs of the form (row value, column value).

More generally, a Cartesian product of n sets, also known as an n-fold Cartesian product, can be represented by an array of n dimensions, where each element is an n-tuple. An ordered pair is a 2-tuple or couple.

The Cartesian product is named after René Descartes, whose formulation of analytic geometry gave rise to the concept, which is further generalized in terms of direct product.

Cis–trans isomerism

Cis–trans isomerism, also known as geometric isomerism or configurational isomerism, is a term used in organic chemistry. The prefixes "cis" and "trans" are from Latin: "this side of" and "the other side of", respectively. In the context of chemistry, cis indicates that the functional groups are on the same side of the carbon chain while trans conveys that functional groups are on opposing sides of the carbon chain. Cis-trans isomers are stereoisomers, that is, pairs of molecules which have the same formula but whose functional groups are rotated into a different orientation in three-dimensional space. It is not to be confused with E–Z isomerism, which is an absolute stereochemical description, and only to be used with alkenes. In general, stereoisomers contain double bonds that do not rotate, or they may contain ring structures, where the rotation of bonds is restricted or prevented. Cis and trans isomers occur both in organic molecules and in inorganic coordination complexes. Cis and trans descriptors are not used for cases of conformational isomerism where the two geometric forms easily interconvert, such as most open-chain single-bonded structures; instead, the terms "syn" and "anti" would be used.

The term "geometric isomerism" is considered by IUPAC to be an obsolete synonym of "cis–trans isomerism".

Community Z Tools

The Community Z Tools (CZT) initiative is based around a SourceForge project to build a set of tools for the Z notation, a formal method useful in software engineering. Tools include support for editing, typechecking and animating Z specifications. There is some support for extensions such as Object-Z and TCOZ. The tools are built using the Java programming language.

CZT was proposed by Andrew Martin of Oxford University in 2001.

E–Z notation

E–Z configuration, or the E–Z convention, is the IUPAC preferred method of describing the absolute stereochemistry of double bonds in organic chemistry. It is an extension of cis–trans isomer notation (which only describes relative stereochemistry) that can be used to describe double bonds having two, three or four substituents.

Following the Cahn–Ingold–Prelog priority rules (CIP rules), each substituent on a double bond is assigned a priority.

If the two groups of higher priority are on opposite sides of the double bond, the bond is assigned the configuration E (from entgegen, German: [ɛntˈɡeːɡən], the German word for "opposite").

If the two groups of higher priority are on the same side of the double bond, the bond is assigned the configuration Z (from zusammen, German: [tsuˈzamən], the German word for "together").

The letters E and Z are conventionally printed in italic type, within parentheses, and separated from the rest of the name with a hyphen. They are always printed as full capitals (not in lowercase or small capitals), but do not constitute the first letter of the name for English capitalization rules (as in the example above).

Another example: The CIP rules assign a higher priority to bromine than to chlorine, and a higher priority to chlorine than to hydrogen, hence the following (possibly counterintuitive) nomenclature.

For organic molecules with multiple double bonds, it is sometimes necessary to indicate the alkene location for each E or Z symbol. For example, the chemical name of alitretinoin is (2E,4E,6Z,8E)-3,7-dimethyl-9-(2,6,6-trimethyl-1-cyclohexenyl)nona-2,4,6,8-tetraenoic acid, indicating that the alkenes starting at positions 2, 4, and 8 are E while the one starting at position 6 is Z.

Fastest

Fastest is a model-based testing tool that works with specifications written in the Z notation. The tool implements (Cristia & Rodriguez Monetti 2009) the Test Template Framework (TTF) proposed by Phil Stocks and David Carrington in (Stocks & Carrington 1996). It is freely available online.

General set theory

General set theory (GST) is George Boolos's (1998) name for a fragment of the axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms.

Jean-Raymond Abrial

Jean-Raymond Abrial (born 1938) is a French computer scientist and inventor of the Z and B formal methods.

J.-R. Abrial is the father of the Z notation (typically used for formal specification of software), during his time at the Programming Research Group within the Oxford University Computing Laboratory (now Oxford University Department of Computer Science), and later the B-Method (normally used for software development), two leading formal methods for software engineering. He is the author of The B-Book: Assigning Programs to Meanings. For much of his career he has been an independent consultant, as much at home working with industry as academia. Latterly, he became a Professor at ETH Zurich in Switzerland.

Maplet

A maplet or maplet arrow (symbol: ↦, commonly pronounced "maps to") is a symbol consisting of a vertical line with a rightward-facing arrow. It is used in mathematics and in computer science to denote functions (the expression x ↦ y is also called a maplet). One example of use of the maplet is in Z notation, a formal specification language used in software development.In the Unicode character set, the maplet is at the point U+21A6.

Michael Spivey

Michael Spivey (commonly known as Mike Spivey) is a British computer scientist at the University of Oxford.

Spivey was born in 1960 and educated at Archbishop Holgate's Grammar School in York, England. He studied mathematics at Christ's College, Cambridge and then undertook a DPhil in computer science on the Z notation at Wolfson College, Oxford and the Programming Research Group, part of the Oxford University Computing Laboratory.

Mike Spivey is a University Lecturer in Computation at the Oxford University Department of Computer Science and Misys and Anderson Fellow of Computer Science at Oriel College, Oxford. His main areas of research interest are compilers and programming languages, especially logic programming. He wrote an Oberon-2 compiler.

Mondex

Mondex is a smart card electronic cash system, implemented as a stored-value card.

Mondex was conceived by Tim Jones and Graham Higgins of the National Westminster Bank in the United Kingdom. The system was initially developed between 1990 and 1993, with internal trials being carried out by approximately 6,000 London-based NatWest staff from 1992. The system was publicly unveiled in December 1993. Initial public trials of the payment system were carried out from July 1995, by the newly incorporated Mondex International in Swindon, Wiltshire. The public phase had required the development and manufacture of numerous merchant devices and smart cards, with BT, NatWest and the Midland Bank sponsoring and installing retail terminals at the car parks, payphones, buses and 700 of the merchants in the town, and issuing Mondex cards to the residents. The system was subsequently sold to MasterCard International in 2001. MasterCard by then already owned 49% of the company.

Mondex launched in a number of markets during the 1990s, expanding from the original trial in Swindon to Hong Kong, New York and Guelph, Canada. It was also trialled on several British university campuses from the late 1990s, including the University of Edinburgh, University of Exeter (between 1997 and 2001), University of York, University of Nottingham, Aston University and Sheffield Hallam University. Mondex's Canadian pilot ended after three years, in 1998, when partners backed out.The Z notation was used to prove security properties about Mondex, allowing it to achieve ITSEC level E6, ITSEC's highest granted security-level classification.

Object-Z

Object-Z is an object-oriented extension to the Z notation developed at the University of Queensland, Australia.

Object-Z extends Z by the addition of language constructs resembling the object-oriented paradigm, most notably, classes. Other object-oriented notions such as polymorphism and inheritance are also supported.

While not as popular as its base language Z, Object-Z has still received significant attention in the formal methods community, and research on aspects of the language are ongoing, including hybrid languages using Object-Z, tool support (e.g., through the Community Z Tools project) and refinement calculi.

S (set theory)

S is an axiomatic set theory set out by George Boolos in his 1989 article, "Iteration Again". S, a first-order theory, is two-sorted because its ontology includes “stages” as well as sets. Boolos designed S to embody his understanding of the “iterative conception of set“ and the associated iterative hierarchy. S has the important property that all axioms of Zermelo set theory Z, except the axiom of extensionality and the axiom of choice, are theorems of S or a slight modification thereof.

Set-builder notation

In set theory and its applications to logic, mathematics, and computer science, set-builder notation is a mathematical notation for describing a set by enumerating its elements or stating the properties that its members must satisfy.Defining sets by properties is also known as set comprehension, set abstraction or as defining a set's intension.

Set-builder notation is sometimes simply referred to as set notation, although this phrase may be better reserved for the broader class of means of denoting sets.

Tie (typography)

The tie is a symbol in the shape of an arc similar to a large breve, used in Greek, phonetic alphabets, and Z notation. It can be used between two characters with spacing as punctuation, or non-spacing as a diacritic. It can be above or below, and reversed. Its forms are called tie, double breve, enotikon or papyrological hyphen, ligature tie, and undertie.

Z

Z (named zed or zee ) is the 26th and final letter of the modern English alphabet and the ISO basic Latin alphabet.

Z User Group

The Z User Group exists to promote use and development of the Z notation, a formal specification language for the description of and reasoning about computer-based systems. It was formally constituted on 14 December 1992 during the ZUM'92 Z User Meeting in London, England.

ISO standards by standard number
1–9999
10000–19999
20000+
IEC standards
ISO/IEC standards
Related

This page is based on a Wikipedia article written by authors (here).
Text is available under the CC BY-SA 3.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.