search

septract / starling-tool

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

Conditional views without else #126

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

Add

{| if P then X |}

as syntactic sugar for

{| if P then X else emp |}

Example: optimistic set has a lot of redundant else going on.

MattWindsor91 commented 7 years ago

The false-view-and-assert branch has this.