Method-local invariants?

[MattWindsor91]

One for the 'would be nice' pile: some syntax like

method foo(int bar, bool baz) invariant {| P(bar) * Q(bar, baz) |} {
    {| X() |} ... {| Y() |}
}

which is syntactic sugar for

method foo(int bar, bool baz) invariant {| P(bar) * Q(bar, baz) |} {
    {| P(bar) * Q(bar, baz) * X() |} ... {| P(bar) * Q(bar, baz) * Y() |}
}

This would clean up a few methods where we need special information about the incoming parameters to pass through the entire method body. There are some examples in the GRASShopper stuff.

[MattWindsor91]

One thing this doesn't really help us with is when we need to thread through information about parameters in a way that changes view throughout the method (thread state machines, etc).