Hi!
I submitted a PR #4 with a solution to the challenge. Ran so fast that misplaced where should I put the prover reports and put them in the PR. Pasting them also here:
A run of the new BordaMissingRule.spec on the original Borda.sol that is verified is here
A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug is here
Reports of all previously acknowledged bounty specs on BordaNewBug.sol, these specs will be found in the bounty_specs folder: none
A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug is here
It was really fun, learned a bunch on CVL grammar and invariant thinking. Thanks a lot :)
Hi!
I submitted a PR #4 with a solution to the challenge. Ran so fast that misplaced where should I put the prover reports and put them in the PR. Pasting them also here:
A run of the new
BordaMissingRule.specon the original Borda.sol that is verified is hereA run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug is here
Reports of all previously acknowledged bounty specs on BordaNewBug.sol, these specs will be found in the bounty_specs folder: none
A run of
BordaMissingRule.speconBordaNewBug.solshowing your rule catches the bug is hereIt was really fun, learned a bunch on CVL grammar and invariant thinking. Thanks a lot :)