We will study and practice with two
different type of specification languages that are often used in conjunction for describing
different aspects of systems: the notation Z, which is
suitable for describing transformational aspects, i.e. how the actions of a
system operate on data; and the process language CSP,
which allows to describe the reactive behaviour of systems, i.e. the
processes as part of which actions are executed and the communication
channels through which processes communicate.
Both
languages come with various tools to verify properties of the
specifications and to help in the refinement process from specification to program.
