Are verify and measure-complexity different? about dafny HOT 6 CLOSED

Well, actually I see that dafny 4.6 seems to neuter the --boogie options, so using them to create my own faux-measure-complexity on top of verify as I did on 4.4 is no longer possible.

So maybe that's (part of?) the answer: until recently measure-complexity and verify were very similar but the plan is to diverge?

from dafny.

@atomb

from dafny.

There's different ways of preventing proof complexity. A simple one is to limit the maximum resources used by a proof. This option is available in dafny verify, using --resource-limit <resource-limit>.

A more complicated way of preventing proof complexity is to run multiple iterations and to compare the resources used by each iteration. I did not want to increase the scope of dafny verify by adding options related to this statistical technique, so I added a separate command, measure-complexity, for doing that. The scope of measure-complexity is not entirely clear. In the future it might even be implemented in a separate repository as a plugin for the Dafny CLI.

Also I think the default behavior of measure-complexity should be quite different from verify. For example,dafny verify returns a success exit code if everything verified in a single iteration. measure-complexity currently returns a success code if everything verified in each iteration, but I intend to change that so that it only returns a success exit code if the relative standard deviation of the resource count used is within a a certain bound.

from dafny.

Thank you for the explanation.

I mentioned --filter-symbol being available in verify but not in measure-complexity. It would be very useful in there too, to accelerate iterating. Will it be made available there too?
(Should I open a new issue?)

from dafny.

Thank you for the explanation.

I mentioned --filter-symbol being available in verify but not in measure-complexity. It would be very useful in there too, to accelerate iterating. Will it be made available there too? (Should I open a new issue?)

In nightly, these options are already available for measure-complexity

from dafny.

Thank you!

from dafny.