Unusual help needed wrt arithmetic

Feb 27, 2014 at 1:30 AM
Edited Feb 27, 2014 at 1:30 AM
Hi everyone,

At http://rise4fun.com/Dafny/aZCF is a short program whose correctness depends on ceilings and floors, i.e. the functions that take real numbers to the least higher resp greatest lower integer.

At one point (identified by the comment "Why does it need this?") a strange bit of help is required for the prover to realise that if k>0 then k-1>=0. (I'm sure it does realise that, but it has to realise that at the right moment :-)

If the help is commented out, then the prover times out.

Any suggestions about how that step could be taken more neatly?


PS --- Apologies for the typo "Handong" --- it should be "Handing".