Dr.F.J. de Vries
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.