Currently, our @ast rule annotation generates a bunch of procedures for side-conditions, but deletes the proc of the annotated loop itself. This leads to confusing situations because one can choose the invariant to be I = false, and still have the proc verify. See the discussion here: #97 (reply in thread).
Instead of the deleting the proc, we should replace the loop by assert [I]; havoc vars; validate; assume [I], i.e. the "obvious" spec for the loop with invariant I. This would force the user to add a pre of ?(false) to the proc, making very clear what is shown (here: nothing useful).
Unfortunately, this diverges even further from the officially published version of the AST rule. I'd really like to see a formal proof that this new encoding is still sound.
Currently, our
@astrule annotation generates a bunch of procedures for side-conditions, but deletes theprocof the annotated loop itself. This leads to confusing situations because one can choose the invariant to beI = false, and still have the proc verify. See the discussion here: #97 (reply in thread).Instead of the deleting the proc, we should replace the loop by
assert [I]; havoc vars; validate; assume [I], i.e. the "obvious" spec for the loop with invariantI. This would force the user to add a pre of?(false)to the proc, making very clear what is shown (here: nothing useful).Unfortunately, this diverges even further from the officially published version of the AST rule. I'd really like to see a formal proof that this new encoding is still sound.