The Single Transferable Voting System: Functional Decomposition in Formal Specification

A formal specification is presented in the Z language for a simplified version of the Single Transferable Vote form of election. This is a correctness-critical application which is one of a class of related and interesting applications, i.e. electoral models. This specification is based on the form of election defined by the Students' Representative Council of the University of Cape Town , and demonstrates the utility of formal specification for requirements validation. A succinct statement of the algorithm is given using the schema calculus. The specification provides a vehicle for contributing to the current debate on good Z specification style. Brief discussion of specification styles in the literature sets the context for an overview style employed here, one of functional decomposition.