Contents
A Glossary of the Formal Specification Language Z
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).
. . . . . . . . . ( end of section Z Glossary) <<Contents | End>>
End