A Glossary of the Formal Specification Language Z

Spivey 89, J M Spivey, the Z Notation: A Reference Manual, PHI 1989.
1. abstraction_schema::= In data refinement a schema that documents the relationship between abstract and concrete state spaces.
2. basic_type::=A named type denoting a set of objects regarded as atomic in a specification.
3. binding::=an object with one or more components named by identifiers. An element of a schema type.
4. cartesian_product_type::=a type containg n-tuples of objects drawn from other type.
5. constraint::=a property that values of variables must satisfy to fit a decalration.
6. data_refinement::=the process of showing that one set of operations is implementd by another set on a different state space.
7. derived_component::=A component of a schema describing the state space of an abstract data type whose value can be deduced from values of the othe components.
8. extension::@(situation,situation)=/restriction.
9. finitary::=??.
10. graph::=the set of ordered pairs of objects that satisfy a binary relation.
11. implicit_pre_condition::=A precondition that is not explicitly stated in a specification but is implicitly part of the post_condition or of the invariant of the final state.
12. join::=two typecompatible signatures can be joined to forma a signature that has all variables of both the original ones paired with the same types.
13. logically_equivalent::@(predicates,predicates)=expressing the same property, that is when they are true in exactly the same conditions.
14. loose_specification::=a spcification where the values of the global variables are not completely determined by the predicates that constrain them.
15. non_deterministic::=an operation in an abstract data type where there may be more than one possible state after for each single state befor it.
16. operation_refinement::=the process of showing that one operation is implemented by another with the same state space.
17. pre_condition::=the condition on a state before an operation and on its inputs that there should exist a possible state afterwards and outputs satisfying its post_condition.
18. predicate::=a formula describing a relationship between values of the variables in a signature.
19. prperty::= the mathematical relationship expresses by a predicate characterized by the situations in which the predicate is true.
20. restriction::@(situation,situation)= signature(2nd) is a subsignature (1st) and each variable in signature(2nd) has the same value as it has in the (1st) signature.
21. relation::=??.
22. schema_type::=a type contain bindings with name components drawn from other types.
23. scope_rules::=rules that determine what identifiers may be used at each point in a specification and what definition each identifier refers to.
24. sequential_composition::operation.syntax><operation.syntax->operation.syntax= (1st) bold_semicolon (2nd).
25. sequential_composition::=the operation where (1st) occurs imediatly before (2nd).
26. set_type::types->types=the sets of objects of type (_).
27. signature::variables<>->type.
28. situation::=that which determines the values of variables in a signature.
29. state_space::=the set of possible states.
30. sub_signature::@(signature,signature)=(==>).
31. type::=used to determine the set of values that an expression can take.

    Z types are of 4 kinds:

32. type>==set(basic_type, set_type, cartesian_product_type, schema_type).

. . . . . . . . . ( end of section Z Glossary) <<Contents | End>>