We have converted the English specification of the Hare-Clark method given in the Electoral Act 1992 into a logical specification which is mechanically manipulable by the HOL theorem prover. The specification is available as a PDF file.
The ACT Electoral Commission provides the eVACS source code for public scrutiny at http://www.elections.act.gov.au/Elecvote.html to ensure appropriate transparency. However, only an incomplete representation of the eVACS code is available and there is no immediate way to build or test this code.
We built the test harness required to run some of this code and tested the eVACS vote counting module against real and invented data. We found a bug in the results reported for our Teletubbies test election data. The ACT Electoral Commission and Software Improvements have acknowledged, traced, and fixed this bug. Note this bug was found with only minimal scrutiny of the code fragments of the eVACS system. It is quite feasible that a more detailed scrutiny could expose other bugs.
We also spent four to five hours scanning the code and performing a brief code review. Notably there is little documentation, the counting system is difficult to fathom, and while some of this is due to the complexity of the Hare-Clark method, the construction of the code omits basic software engineering concepts that encourage maintainability and make it understandable. While these secondary issues may result from initial design, the overall impression is that they probably result from the code being completed in a limited amount of time.
These findings reinforce our belief that this vote counting program does not wholly meet the formal specification, documentation, and formal correctness standards required for such an important task. We therefore intend to provide an in-house vote counting program, written in Standard ML, which will be verified against the logical specification of Hare-Clark which we have developed.
We are currently rewriting the original Standard ML vote counting program to make it manipulable by a mechanical theorem prover. Once this is complete we shall verify its correctness against the formal specification of Hare-Clark that was developed for this investigation. We expect to report on this work in the near future.
To ensure that our formalisation correctly captures the ACT Hare-Clark legislation we require input from the ACT Electoral Commission.
|
Site Map and Table of Contents |
Disclaimer |
Page content Copyright 2003 NICTA
|