[PUBLIC HI-LITE] ada-evoting 0.1 available

Yannick Moy moy at adacore.com
Mon Jun 4 17:27:45 CEST 2012


On 06/03/2012 08:14 PM, David MENTRE wrote:
> Hello,
>
> Following latest Hi-Lite meeting and as several people asked me for
> the source code, here is the release 0.1 of my "ada-evoting"
> electronic voting booth program:
>    http://www.linux-france.org/~dmentre/code/ada-evoting-0.1.tar.gz
>
> The program builds with gnat GPL Edition 2011 and is partially
> verified with GNATprove 0.2w. Currently, two VCs are not proved,
> therefore I still consider the program buggy in both contracts and
> code. I nonetheless release it otherwise it might never be done. ;-)
>    evoting.adb:243:25: range check not proved
>    evoting.ads:110:13: postcondition not proved

Hi David,

Thanks for making this example publicly available, I have added it to 
the examples distributed with Hi-Lite (too late for the first GPL 
release, but in the next one!).

Claire and I have added the necessary loop invariants to prove the 
postcondition, and corrected your code/annotations in minor ways. See 
the files attached:
- Total_Range_t must be slightly bigger to prevent the possible range 
check error you reported.
- The quantification in the postcondition must be restricted to 
1..Last_Candidate to exclude the special case "No Vote" (index value 0) 
and values beyond Last_Candidate for which the count is not known.
- An else part must be added to the if-statement in Compute_Winners, to 
set winners(i) to False.
- Loop invariants are added in Compute_Winners.

Right now, the 2 VCs you reported are proved only when a special option 
of Alt-Ergo is used (-redondance 4) which allows triggers to be 
considered. The issue is that Alt-Ergo compute triggers to instantiate 
the quantified formulas in the loop invariants. By default, Alt-Ergo 
computes 2 triggers only, and it happens on your code that these 
triggers are not the right ones to prove the VCs, hence the option 
-redondance 4 to increase the number of computed triggers. We have 
looking at a way to automatically instruct Alt-Ergo to keep all the 
possible triggers for quantified formulas from user code (loop 
invariants, pre/postconditions), so that your code is proved without 
using this special switch.

Note that the postcondition involving Counters_Sum is not proved, as 
Counters_Sum has no logical definition (no postcondition here, but 
really we'd like an axiomatization of Counters_Sum). This is something 
we'd like to improve this year.

Best regards,

-- 
Yannick Moy, Senior Software Engineer, AdaCore

-------------- next part --------------
A non-text attachment was scrubbed...
Name: evoting.ads
Type: text/x-adasrc
Size: 5621 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/hi-lite-discuss/attachments/20120604/e35ab0d1/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: evoting.adb
Type: text/x-adasrc
Size: 11817 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/hi-lite-discuss/attachments/20120604/e35ab0d1/attachment-0001.bin>


More information about the Hi-lite-discuss mailing list