Please enable JavaScript.
Coggle requires JavaScript to display documents.
Introduction to the Z formal Specification language - Coggle Diagram
Introduction to the Z formal Specification language
Z schemas(math decscription)
Introduce specification entities and defines
invariant predicates over these entities
A predicate is a Boolean expression
A way of decomposing a specification into small piece
used to describe 2 aspect of the system
Dynamic
-Operation
-relationship
static
-invariant:relationship that maintained as the system moves from state to state
state of a properly that does not change as the loop execute
can be property of a mathematical objet which remais unchanged after operatios or transformation of certain type are applied to the objects.
State
z as specification language
history
developed at Programming Research Group (Oxford Univesity Computing Laboratory-late 1974)
Jean-Raymond Abrial (the founder of Z notation)
Z stand for Zarmello
Standard mathematical notation=axiomatic set theory
used to describing and modelling in computing systems.
sysmbol for z notation
Key Points
1,Z specifications are made up of a mathematical model of the
system state and a definition of operations on that state
2.A Z specification is presented as a number of
schemas
3.Schemas may be combined to make new schemas
4.Operations are specified by defining their effect on the system
state.
5.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.