Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    The Single Transferable Voting System: Functional Decomposition in Formal Specifications

    1st Irish Workshop on Formal Methods

    Dublin, Ireland. 3rd - 4th July 1997


    M.R. Poppleton


    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.


    PDF filePDF Version of this Paper (183kb)