1
Vote

termination metric

description

http://rise4fun.com/Dafny/yLsls

Why the hover text in MVS says only "decreases" for the outermost while?

comments

jiplucap wrote Oct 11, 2016 at 3:30 PM

I'm sorry I realized now that it is not only the decreases expression, but Dafny is not working properly on the partial correctness of the previous program and also on this one

http://rise4fun.com/Dafny/v5fA

that is obviously incorrect, but Dafny does not detect it.