search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Method-local invariants? #127

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

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 commented 7 years ago

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).