Votail is an implementation of Ireland's method of Proportional
Representation by Single Transferable Vote (PRSTV). The functional
requirements derived from Irish electoral law are specified using
Business Object Notation (BON) and the Java Modeling Language (JML).
Formal methods have been used to verify the correctness of the software.