[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci Dept] / [R J Botting] / [Samples] / z.glossary
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Tue Sep 18 15:27:41 PDT 2007


    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>>