Treffer: Towards the development of an Electoral Count System using formal methods

Techniques which use mathematical principles to develop computer systems are collectively known as Formal Methods. Formal Methods are usually applied to computer systems when correctness and soundness are primarily important. A system to count votes is an example of such a system. This work includes the specification of, and the full development of part of, such an electoral system. When developing the system, a number of interesting issues arose, the examination of which became a significant part of this work. The development of a system using formal methods entails taking a speciGcation, written using mathematics and, moving, step by step, towards eventual implementation. We call these steps refinement steps. There are two main kinds of refinement - data refinement where we move from using abstract data in our descriptions to using more concrete data and algo- rithmic refinement where we introduce programming-like constructs. The traditional strategy is to proceed with data refinement and then with algo- rithmic refinement. In this thesis a strategy of mixing these approaches is examined, e.g. applying algorithmic refinement first. This strategy is found to be useful and to result in elegant solutions. A fundamental tenet of refinement is that at each point in the develop- mental cycle (including the starting specification and the eventual imple- mentation), the user should be unaware of any 'behind the scenes' activity. This means that the interface to the user should not change. However, it may happen that part of the specification is written in terms of parame- terised abstract data. Then data refinement will change the interface. This issue is examined in this work and a workaround is provided for checking the correctness of this tricky refinement step. Two paths of development are used in the work. The first is that of using Z and Morgan's Refinement Calculus. The B Method is then used for the main part of the thesis. The specification of the systems are w