search

septract / starling-tool

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

Underscore placeholder variable #111

Closed septract closed 7 years ago

septract commented 7 years ago

It would be useful to be able to write _ for an existentially-quantified placeholder. Eg. in lclist-grasshopper: 

{| isList(v) * has1Lock(curr, _) * isVal(curr, cv) |}

Right now I'm declaring _ as a named variable, but this doesn't have the right semantics. E.g. 

{| foo(x,_) * bar(y,_) |}

This requires the second arguments of foo and bar to be equal.

This is a relatively safe use of existential quantification (basically a 'don't-care' quantification) so it shouldn't blow up Z3 or HSF.

How hard would it be to add this, @CaptainHayashi?

MattWindsor91 commented 7 years ago

Duplicate of #28, I think. Will comment on there.