Please enable JavaScript.
Coggle requires JavaScript to display documents.
INTRODUCTION TO THE Z FORMAL SPECIFICATIONS LANGUAGE, WAN NUR AFIQAH BINTI…
INTRODUCTION TO THE Z FORMAL SPECIFICATIONS LANGUAGE
Schemas (specification building block)
dynamic
relationship
changes of state
operation
static
state
invariant
value - consistent - process (math)
A formal specification notation based on
set theory
Z schemas
introduce specification entities and defines invariant predicates over these antities
A predicate is a Boolean expression
Some predcates can have side-effects that change the state of the entities involved
Schemas can be include in other schemas and may act as type definitions
Name are local to schemas
In many respects, Z schemas are akin to objects
Z = Zermelo
developed under the guidance of of ISO
Graphical presentation of schemas make Z specification easier to understand
Mathematical notation of schemas allows the building of formal completeness and consistency proofs to validate the specification
The Z notation
a schema includes
a
name
ientifying the schema
A
signature
introducing entities and their types
A predicate part defining relationships between the entities in the signature by stating a logical expression which must always be true (an invariant)
Z Conventions
A schema name prefixed by the Greek letter Delta, means that the operation changes some or all of the state variables introduced in that schema
A variable name decorated with a ? represents an input
A variable name decorated with a quote mark (N') represents the value of the state variable N after an operation
A schemaa name prefixed by the Greek letter Xi means that the defined operation does not change the values of state variables
A variable name decorated with a ! represents an output
KEY POINTS
Z specifications are made up of a mathematical model of the system state and definition of operations on that state
A Z specification is presented as a number of schemas
Schemas may be combined to make new schemas
Operations are specified by defining their effect on the system state
Operations may be specified incrementally. Different schemas can be combined to complete the specification
The notation used is very cryptic, though great effort is made toward understandability
A container specification
An indicator specification
Z symbols
WAN NUR AFIQAH BINTI ZULKEFLI (D20191089434)
