Z notation
View on Wikipediafrom Wikipedia
The Z notation /ˈzɛd/ is a formal specification language used for describing and modelling computing systems.[1] It is targeted at the clear specification of computer programs and computer-based systems in general.
History
[edit]In 1974, Jean-Raymond Abrial published "Data Semantics".[2] 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), working with Bertrand Meyer, Abrial also worked on developing Z.[3] The Z notation is used in the 1980 book Méthodes de programmation.[4]
Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer.[5] 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!"[6] although the name "Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory.
In 1992, the Z User Group (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences.[7]
Usage and notation
[edit]Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic.[8] 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. 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.[9]
Standards
[edit]ISO completed a Z standardization effort in 2002. This standard[10] and a technical corrigendum[11] are available from ISO free:
Award
[edit]In 1992, Oxford University Computing Laboratory and IBM were jointly awarded The Queen's Award for Technological Achievement "for the development of ... the Z notation, and its application in the IBM Customer Information Control System (CICS) product."[12]
Further reading
[edit]- 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. Archived from the original on 5 April 2007. Retrieved 22 March 2006.
- Bowen, Jonathan (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press, International Thomson Publishing. 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.
- Ince, D. C. (1993). An Introduction to Discrete Mathematics, Formal System Specification, and Z. Oxford University Press. doi:10.1093/oso/9780198538370.001.0001. ISBN 978-0198538370.
See also
[edit]- Z User Group (ZUG)
- Community Z Tools (CZT) project
- Other formal methods (and languages using formal specifications):
- Fastest, a model-based testing tool for the Z notation
- Unified Modeling Language, a software system design modeling tool by Object Management Group
References
[edit]- ^ Bowen, Jonathan P. (2016). "The Z Notation: Whence the Cause and Whither the Course?" (PDF). Engineering Trustworthy Software Systems. Lecture Notes in Computer Science. Vol. 9506. Springer. pp. 103–151. doi:10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
- ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
- ^ Hoare, Tony (2011). "Greetings to Bertrand on the Occasion of his Sixtieth Birthday" (PDF). In Nanz, Sebastian (ed.). The Future of Software Engineering. Springer. pp. 183–184. doi:10.1007/978-3-642-15187-3. ISBN 978-3-642-15187-3.
- ^ Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (in French), Eyrolles
- ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M. (eds.), On the Construction of Programs, Cambridge University Press, ISBN 0-521-23090-X (describes early version of the language).
- ^ Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.
- ^ Bowen, Jonathan (July 2022). "The Z User Group: Thirty Years After" (PDF). FACS FACTS. No. 2022–2. BCS-FACS. pp. 50–56. Retrieved 3 August 2022.
- ^ Spivey, J. Michael (1992). The Z Notation: A Reference Manual. International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall. ISBN 978-0139785290.
- ^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites". unicode-search.net. Archived from the original on 24 March 2020. Retrieved 24 March 2020.
- ^ a b c "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 1 July 2002. 196 pp.
- ^ 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. 15 July 2007. 12 pp.
- ^ "The Queen's Award for Technological Achievement 1992". Oxford University Computing Laboratory. Archived from the original on 2 December 2008. Retrieved 17 October 2021.
| International | |
|---|---|
| National | |
| Other | |
Z notation
View on Grokipediafrom Grokipedia
Overview
Definition and Purpose
Z notation is a model-oriented formal specification language based on Zermelo-Fraenkel set theory and first-order predicate logic, designed to describe the behavior and structure of computing systems in an unambiguous, mathematical manner.[5] It enables the construction of abstract models that capture essential system properties without implementation details, facilitating clear and precise documentation of requirements.[6] The primary purpose of Z notation is to support the specification of software and hardware systems, allowing for early detection of design errors through rigorous analysis, refinement of abstract models into concrete implementations, and formal verification via mathematical proofs.[5] Unlike executable programming languages, Z is intended solely for reasoning and validation, not direct execution, thereby promoting reliability in system development.[5] Z notation is targeted at software engineers and system designers working on complex, high-stakes applications, especially safety-critical domains such as railway signaling, medical devices, and nuclear power systems.[5] By contrast with informal natural language methods, which often introduce ambiguities, Z enforces mathematical precision to ensure requirements are complete and consistent.[5] Specifications are typically organized using schemas as a structuring mechanism to define state spaces and operations reusably.[5]Key Features
Z notation's schema notation provides a modular framework for structuring formal specifications, encapsulating declarations of variables, predicates defining properties, and operations within boxed schemas that can be reused and composed using a schema calculus. This approach allows for the definition of state schemas, which describe the system's variables and invariants, and operation schemas, which specify inputs, outputs, and state transitions as relations between pre- and post-states. For instance, schemas can be combined via conjunction to merge components or disjunction to model alternatives, promoting reusability and hierarchical decomposition without procedural details.[2][7] The declarative style of Z emphasizes specifying what a system must achieve rather than how it operates, relying on mathematical predicates to express preconditions that must hold before an operation, postconditions describing the resulting state, and invariants that persist across operations. This model-oriented approach, grounded in set theory, enables precise description of system behaviors through relations, facilitating analysis of properties like safety and liveness without committing to implementation choices.[7][2] Z is designed with mechanized analysis in mind, incorporating a type system that supports automated type-checking to ensure consistency and a syntax conducive to theorem proving for verifying specification properties. Tools can parse schemas, compute preconditions, and assist in refinement, making it suitable for rigorous development processes.[7][2] Modern adaptations of Z leverage Unicode for direct rendering of mathematical symbols such as ∈ (membership), ∪ (union), and λ (lambda abstraction), alongside LaTeX markup for typesetting specifications in digital environments. The ISO/IEC 13568 standard defines concrete syntax with LaTeX commands (e.g.,\in for ∈) and Unicode code points (e.g., U+2208 for ∈), enabling integration with tools for parsing, editing, and visualization while maintaining portability across platforms.[5]
Historical Development
Origins
The origins of Z notation trace back to Jean-Raymond Abrial's research at IBM in the early 1970s, where he sought to formalize data modeling to address ambiguities in software system descriptions. In 1974, Abrial published "Data Semantics," a seminal paper presented at the IFIP Working Conference on Data Base Management in Cargèse, Corsica, which introduced a relational model based on binary relations for specifying data structures and their semantics.[8] This work emphasized precise mathematical definitions to bridge the gap between informal requirements and implementation, influencing subsequent formal specification techniques.[9] By 1977, Abrial had begun collaborating with Steve Schuman and Bertrand Meyer at IBM's Vienna Development Center, focusing on extending these ideas to schema-based prototypes for specifying abstract data types. This effort produced the first structured schemas that integrated declarations, predicates, and operations into modular units, enabling hierarchical system descriptions. The collaboration contributed to early works such as the 1979 paper "Specification of Parallel Processes" by Abrial and Schuman.[10] The early motivations for Z notation stemmed from the limitations of informal methods in capturing programming language semantics and ensuring system reliability, drawing inspiration from Edsger W. Dijkstra's advocacy for structured programming to promote clarity and verifiability. It was also shaped by Tony Hoare's axiomatic semantics, which provided a framework for proving program correctness through preconditions and postconditions. These influences aimed to create a notation that supported unambiguous specification while facilitating refinement to code.[11] Key ideas from the collaboration were further disseminated in the 1980 publication "A Specification Language" by Abrial, Schuman, and Meyer, included in the book On the Construction of Programs. This paper formalized the schema concept and its role in specification, marking the transition from internal prototypes to broader academic influence.[10]Evolution at Oxford and Beyond
During the late 1970s and 1980s, Z notation matured significantly at the University of Oxford's Programming Research Group (PRG), where Jean-Raymond Abrial, arriving in September 1979, formalized its foundational elements, including schemas and the associated toolkit for specification and refinement.[12] Abrial's work at the PRG, in collaboration with researchers like Cliff B. Jones, established Z's structure based on set theory and predicate calculus, with early publications from the group documenting its grammar and semantics.[13] Following Abrial's departure in 1981, Jim Woodcock and others at the PRG continued development, refining the notation's logic and schema calculus through internal technical reports and prototypes.[12] In the late 1980s, dissemination efforts accelerated through key publications from Oxford researchers, standardizing Z for teaching and practical use. J. M. Spivey's 1989 paper in the Software Engineering Journal provided a comprehensive introduction to Z, emphasizing its role in specifying information systems and integrating formal mathematics with natural language. This was complemented by subsequent works, such as Woodcock and Davies' 1996 book Using Z: Specification, Refinement, and Proof, which detailed refinement techniques and proof obligations, becoming a cornerstone for Z-based development methodologies.[14] These texts, emerging from PRG efforts, facilitated wider adoption in academia and industry by offering consistent notation and examples. The formation of the Z User Group (ZUG) in 1992 marked a pivotal step in community building, formally constituted during the ZUM'92 workshop in London to promote Z notation, organize annual meetings, and coordinate standardization initiatives.[15] ZUG's activities, including workshops and newsletters, fostered collaboration among users and influenced the evolution of Z tools and extensions, such as those for object-oriented specifications.[16] After the 1990s, Z integrated with refinement tools like the Z/EVES proof assistant, enabling automated verification, though its mainstream industrial use declined amid the rise of automated techniques such as model checking, which offered scalable analysis for concurrent systems.[17] Despite this, Z persists in education for teaching formal specification principles, with courses incorporating it alongside discrete mathematics, and in legacy systems maintenance where its rigorous schemas support long-term documentation.[18] Jean-Raymond Abrial, a primary developer of Z, passed away on 26 May 2024.Mathematical Foundations
Set Theory and Logic Basis
Z notation is fundamentally grounded in Zermelo-Fraenkel set theory (ZF), which provides the axiomatic basis for constructing and manipulating sets to model system states and data structures.[5] In Z, all mathematical objects are treated as sets within this framework, ensuring rigorous definitions without reliance on primitive non-set entities beyond the axioms of ZF, such as extensionality, pairing, union, and separation.[4] This foundation allows specifications to represent states as sets, enabling precise descriptions of properties and transformations through set-theoretic operations.[2] Basic set constructs in Z include set comprehensions of the form , where is a type, is a bound variable, and is a predicate defining the condition for inclusion, yielding a set of type .[5] Power sets are denoted , representing the set of all subsets of a given type , which is essential for modeling collections of elements.[2] Relations are formalized as subsets of Cartesian products, typed as , facilitating the description of mappings between sets without assuming totality or injectivity.[4] Predicate logic in Z employs first-order logic to express assertions and properties over sets, using a two-valued semantics where predicates evaluate to true or false.[5] Quantifiers include the universal , true if holds for every of type , and the existential , true if holds for at least one such .[2] Logical connectives encompass conjunction , disjunction , implication , and negation , allowing complex predicates to be built compositionally from atomic relations.[4] The basic toolkit of Z includes predefined given sets such as for natural numbers (non-negative integers starting from 0) and for integers (positive, negative, and zero).[5] Standard set operators provided are union , intersection , set difference , and membership , which support fundamental manipulations like combining or filtering sets: for example, , where the type is inferred from context.[2] These operators adhere to ZF axioms, ensuring consistency in specifications.[4] Free types in Z are defined using freetype declarations, such ascolour ::= red | green | blue, which introduce abstract sets of atomic elements or structured constructors without internal structure beyond the enumeration, suitable for enumerations (e.g., colors or states) or as placeholders for implementation-specific sorts.[5] Such types are basic given sets in the ZF universe, distinct from constructed sets, and can be used to extend the type system while maintaining set-theoretic purity.[2]
Type System
Z notation employs a strict type discipline to ensure that all expressions are well-formed and meaningful within the context of set theory and predicate logic. Every term in a Z specification is assigned a unique type, which determines the set of possible values it can take, preventing ambiguities and errors such as applying operations to incompatible structures. This system supports polymorphism through generic type parameters, allowing specifications to be reusable across different type instantiations.[2] Basic types in Z are introduced as given sets, which are abstract collections of atomic objects without internal structure, declared using the notation , where each names a distinct basic type. Standard given sets include for booleans, for natural numbers, for integers, for real numbers, and others like for characters, providing a foundation for more complex constructions. These types are assumed to be non-empty and pairwise disjoint unless specified otherwise.[2] Constructed types build upon basic types to form composite structures, including power sets for sets of elements of type , Cartesian products for ordered tuples, sequences for finite ordered lists, functions for total mappings, partial functions , relations , and bags for multisets. These types enable the expression of data structures common in specifications, with type rules ensuring operations like union or composition respect domain and range compatibilities. Polymorphism is achieved via generic types, denoted as where is a type parameter that can be instantiated with any type, allowing definitions like a generic sequence type .[2] Schema types treat schemas as first-class types, representing bindings of declarations and predicates, such as which denotes a pair of schemas capturing before-and-after states for operations, with components like and . A schema type is equivalent to a binding , where the declarations assign types to variables and constrains their values, facilitating modular reuse in larger specifications. This integration allows schemas to be used in expressions, such as passing a schema-valued variable to a generic operation.[2] Type inference in Z derives types automatically from schema declarations and context, using unification to resolve polymorphic parameters—for instance, inferring that applies a function of type . Type checking verifies compatibility throughout the specification, flagging errors like type clashes in schema inclusions or mismatched arguments in function applications, thus maintaining semantic consistency without requiring explicit type annotations in every expression.[2]Core Notation
Schemas
Schemas provide the primary mechanism in Z notation for structuring specifications by encapsulating declarations of variables and their types alongside predicates that constrain their values. A schema is presented in a boxed format, consisting of an optional name, a declaration part separated by a dashed line from a predicate part. The declaration part lists variables with their types or given sets, such asx? : INPUT; state : STATE, while the predicate part specifies logical constraints, for example x? > 0. This structure allows schemas to represent abstract data types, states, and operations in a modular way.[4]
The schema calculus enables the composition of schemas to build more complex specifications. Key operations include conjunction S₁ ∧ S₂, which combines the declarations and conjoins the predicates of two schemas S₁ and S₂; disjunction S₁ ∨ S₂, which offers a choice between the bindings satisfying either schema; hiding, achieved via existential quantification ∃ vars • S to conceal internal variables; renaming S[x/y], which substitutes component names for reuse; and inclusion, where one schema's bindings form a subset of another's. These operations facilitate hierarchical specification construction while preserving type safety and semantic consistency.[4][19]
State schemas define the invariant properties of a system's state. The basic state schema, often named State, declares the state variables and their types along with predicates enforcing the invariant, such as:
State
stateVariables : types
─────────────────
invariant predicates
Init schema, typically Init ≡ State ∧ initialPredicates. Operations on the state are specified using schemas like Op ≡ ΔState ∧ opPredicates, where ΔState denotes the before-and-after state using primed and unprimed variables, ensuring the invariant holds post-operation. This pattern supports reasoning about state transitions.[4]
Generic schemas introduce parameterization for reusability across different types. A generic schema is denoted with type parameters in square brackets, for example [X] SchemaX where X is a generic type, followed by declarations and predicates that may reference X. Instantiation occurs by applying specific types, such as Schemaℕ for natural numbers, allowing abstract specifications of data structures like sequences or sets.[4]
Expressions and Operators
Z notation employs a rich set of operators to construct mathematical expressions, enabling the formal description of data structures and computations within schemas. These expressions are typed according to the underlying type system, ensuring type safety in specifications. The operators are grounded in standard mathematical constructs, primarily from set theory and first-order logic, as standardized in ISO/IEC 13568:2002.[5] Arithmetic expressions in Z operate on numeric types such as natural numbers (ℕ), integers (ℤ), and reals (ℝ). Basic operations include addition (+), which forms a commutative group with identity 0; subtraction (-), defined as $ i - j = i + (-j) $; multiplication (×), forming a commutative ring with identity 1; and division (÷), restricted to non-zero divisors. For example, $ 2 + 3 = 5 $ and $ 10 \div 2 = 5 $. Additionally, the modulo operator (mod) satisfies $ 0 \leq i \mod j < j $ for positive j, as in $ 10 \mod 3 = 1 $, while the floor function $ \lfloor x \rfloor $ yields the greatest integer less than or equal to x, such as $ \lfloor 3.7 \rfloor = 3 $. These operators are total on appropriate domains and are detailed in the mathematical toolkit of the Z standard.[5][20] Set expressions form the core of Z's data modeling, leveraging Zermelo-Fraenkel set theory. The empty set is denoted ∅, equivalent to { x : X \mid \false } for any type X. A singleton set containing a single element e is written as { e }. Set comprehensions allow defining subsets via the syntax { x : Type \mid P \bullet e }, where Type declares the range, P is a predicate, and e is the binding expression; for instance, { x : ℕ \mid x > 0 } denotes the positive naturals. Union (∪) combines sets as { x : X \mid x \in A \lor x \in B }, and intersection (∩) selects common elements as { x : X \mid x \in A \land x \in B }, with examples like {1,2} ∪ {2,3} = {1,2,3}. These constructs support extensible and modular set operations in specifications.[5][20] Logical expressions use classical propositional and predicate logic operators to form predicates. Negation (¬) inverts truth values, so ¬true = false. Conjunction (∧) is true only if both arguments hold, as in P ∧ Q; disjunction (∨) is true if at least one holds, P ∨ Q. Implication (⇒) evaluates to true unless the antecedent is true and consequent false, exemplified by ∀x : X • P(x) ⇒ Q(x); equivalence (⇔) holds when both have the same truth value, P ⇔ Q. Equality (=) between expressions e₁ and e₂ means e₁ ⊆ e₂ ∧ e₂ ⊆ e₁ for sets, or identical values otherwise, while inequality (≠) is ¬(e₁ = e₂). These operators enable precise constraint definitions, with precedence following standard mathematical conventions.[5][20] Function and relation notation in Z treats functions as partial mappings (X ⇸ Y) and relations as sets of pairs. Function application is written f(x), yielding y if (x ↦ y) ∈ f, as in successor(x) = x + 1 for successor : ℕ ⇸ ℕ. The range of a function or relation f is ran f = { y \mid \exists x : dom f • f(x) = y }. The inverse of a relation r, denoted r⁻¹ or r∼, reverses pairs, so { x ↦ y }⁻¹ = { y ↦ x }. Lambda expressions define functions anonymously as λx : Type • e, such as λn : ℕ • n + 1, which maps each natural n to its successor. These notations facilitate reusable and composable descriptions of transformations.[5][20] Sequence and bag expressions handle ordered and multisets. For finite sequences s = ⟨s₁, ..., sₙ⟩, head s returns the first element s₁, provided s ≠ ⟨⟩; tail s yields the subsequence ⟨s₂, ..., sₙ⟩. The cardinality operator #s computes the length n for sequences or the total multiplicity for bags, as in #⟨1,2,1⟩ = 3. These operators, part of the sequence toolkit, support modeling of lists and collections with duplicates, essential for specifying dynamic data structures.[5][20]Usage in Specification
Specification Process
The specification process in Z notation involves a structured methodology for developing formal descriptions of systems, starting from high-level requirements and progressing through refinement to more implementable designs. This process emphasizes mathematical rigor to ensure clarity, consistency, and verifiability, using schemas to encapsulate state definitions and operations.[7] The approach is iterative, allowing specifications to evolve while maintaining formal properties through proofs.[2] The initial step focuses on modeling the abstract state of the system. This entails defining the key variables and their types within a state schema, capturing the essential data structures without implementation details such as data representation or efficiency concerns.[7] Invariants are then specified as predicates within this schema, establishing constraints that must hold true for all valid states, thereby defining the observable behavior and ensuring system consistency.[2] Operations are subsequently described using schemas that include preconditions to guard applicability, postconditions to specify state changes, inputs, and outputs, often employing primed variables to denote the post-state.[7] These elements collectively form an abstract specification that prioritizes what the system does over how it is implemented.[2] Refinement bridges the abstract specification to concrete designs through a series of transformations that preserve correctness. Data refinement relates abstract and concrete models via a retrieve relation, which maps concrete states to their abstract counterparts, enabling the verification that the concrete implementation simulates the abstract behavior.[21] Correctness is ensured by simulation rules: forward simulation requires that the concrete precondition implies the abstract one via the retrieve relation and that the concrete post-state simulates the abstract post-state, while backward simulation imposes totality on the retrieve relation and verifies input-output preservation.[21] This process allows stepwise replacement of abstract data types with concrete ones, such as sequences with arrays, while maintaining invariants and operation semantics.[7] Specifications are organized hierarchically, beginning with a top-level system schema that integrates the overall state and key operations.[2] Decomposition into subsystems occurs through schema calculus operators, such as conjunction for combining schemas or hiding for modularization, facilitating the breakdown of complex systems into manageable components without altering the global properties.[7] Best practices in the Z specification process include mixing formal mathematical descriptions with informal natural language explanations to enhance readability and accessibility for stakeholders.[2] Iterative refinement, supported by formal proofs of simulation and invariant preservation, is recommended to incrementally develop and validate the specification, detecting inconsistencies early and ensuring traceability from requirements to design.[7]Basic Examples
To illustrate the use of Z notation in specifying simple systems, consider a basic file storage system. The state is captured by the FileStore schema, which declares a set of file names and a relation mapping names to their contents, represented as integers (e.g., file sizes or checksums). An invariant ensures no duplicate mappings, meaning each name maps to at most one content value, effectively treating the relation as a partial function.[22]FileStore
files : ℙ Name
contents : Name ↔ ℤ
files = dom contents
∀ n : Name ; c1, c2 : ℤ • n ↦ c1 ∈ contents ∧ n ↦ c2 ∈ contents ⇒ c1 = c2
ℙ denotes the powerset, ↔ a relation, and the invariant predicates maintain consistency by linking the file set to the relation's domain and enforcing uniqueness of mappings per name. This schema defines the abstract state space, grounded in Z's set-theoretic foundations.[22]
Operations on this state are specified via schemas that reference the state before and after execution. For adding a new file, the AddFile operation uses the dashed form ΔFileStore to indicate state change, with inputs marked by ?. It requires the new name not to exist and initializes the content to 0, updating the relation accordingly while preserving the invariant.[22]
AddFile
ΔFileStore
name? : Name
name? ∉ dom files
contents' = contents ∪ {name? ↦ 0}
name? ∉ dom files ensures the operation is only applicable when the file does not already exist; otherwise, it is undefined.[22]
Z notation handles errors or invalid inputs by schemas that leave the state unchanged, using ΞFileStore (pronounced "xi") to bind primed and unprimed variables, indicating no observable change. For instance, if an attempt to add a duplicate file fails, the error-handling schema AddFileError reports the failure without modifying the store.[22]
AddFileError
ΞFileStore
name? : Name
report! : {duplicate}
name? ∈ dom files
Counter
value, limit : ℕ
value ≤ limit