1. Fixed RAC JML warning in Constituency class by rewriting of object invariants. 2. Refactored Alloy model to match architecture of JML specification.
1. Fixed RAC JML warning in Constituency class by rewriting of object invariants.
2. Refactored Alloy model to match architecture of JML specification.

GaloisInc/Votail,GaloisInc/Votail,GaloisInc/Votail