Deprecating statement refinement syntax - #2765

[davidcok]

Fixes #2765, which was part of #2425

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

I'm good with it, but I would prefer to have @RustanLeino provide the final review for that because I don't know the ins and outs of statement refinements

[davidcok]

OK with having Rustan review it, Actually Anjali has called a halt on deprecating stuff, so there will be some strategic conversation before this is merged.

[RustanLeino]

Looks good. I suggest that this PR also deprecate the modify statement.

[davidcok]

Did you mean to deprecate both senses of the modify statement?

[MikaelMayer]

Oh no ! Unless you have an alternative, please don't deprecate the modify statement.
I think the modify statement is actually helpful to modify just the modify behavior of a method. It's makes it possible to debug more easily what's wrong in code where Dafny complains about not being able to modify something.

[davidcok]

Mikael - is it the modify X (i.e. havoc) that you use, or the modify x { } which ought to be modifies and which Rustan proposes to perhaps eventually become do requires... modifies... ensures... { ... }?

[MikaelMayer]

Mikael - is it the modify X (i.e. havoc) that you use, or the modify x { } which ought to be modifies and which Rustan proposes to perhaps eventually become do requires... modifies... ensures... { ... }?

The havoc statement, the first one. I do like the do requires modifies ensures {...} that would be very handy.`

[RustanLeino]

Okay, let's treat the modify statement separately from this PR. I will approve this PR as is.