.Open A Glossary of the Formal Specification Language Z
.Source Spivey 89, J M Spivey, the Z Notation: A Reference Manual, PHI 1989.
abstraction_schema::=` In data refinement a schema that documents the relationship between abstract and concrete state spaces`.
basic_type::=`A named type denoting a set of objects regarded as atomic in a specification`.
binding::=`an object with one or more components named by identifiers. An element of a schema type`.
cartesian_product_type::=`a type containg n-tuples of objects drawn from other type`.
constraint::=`a property that values of variables must satisfy to fit a decalration`.
data_refinement::=`the process of showing that one set of operations is implementd by another set on a different state space`.
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`.
extension::@(situation,situation)=/restriction.
finitary::=`??`.
graph::=`the set of ordered pairs of objects that satisfy a binary relation`.
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`.
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`.
logically_equivalent::@(predicates,predicates)=`expressing the same property, that is when they are true in exactly the same conditions`.
loose_specification::=`a spcification where the values of the global variables are not completely determined by the predicates that constrain them`.
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`.
operation_refinement::=`the process of showing that one operation is implemented by another with the same state space`.
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`.
predicate::=`a formula describing a relationship between values of the variables in a signature`.
prperty::=` the mathematical relationship expresses by a predicate characterized by the situations in which the predicate is true`.
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`.
relation::=`??`.
schema_type::=`a type contain bindings with name components drawn from other types`.
scope_rules::=`rules that determine what identifiers may be used at each point in a specification and what definition each identifier refers to`.
sequential_composition::operation.syntax><operation.syntax->operation.syntax= (1st) bold_semicolon (2nd).
sequential_composition::=`the operation where (1st) occurs imediatly before (2nd)`.
set_type::types->types=`the sets of objects of type (_)`.
signature::variables<>->type.
situation::=`that which determines the values of variables in a signature`.
state_space::=`the set of possible states`.
sub_signature::@(signature,signature)=(==>).
type::=`used to determine the set of values that an expression can take`.

Z types are of 4 kinds:
	type>==set(basic_type, set_type, cartesian_product_type, schema_type).
.Close  Z Glossary