kframework/k — pull request #285 by dwightguth (2014-03-15 21:47:51+00:00)
Title: add negative contracts on KilProperty

Technically the KilProperty contracts are ternary, not binary: a kilproperty can either be required/ensured, or it can be forbidden/destroyed, or it can be unspecified. Trying to implement a ternary EnumSet with an undefined state seemed overkill for this, so I just created negative annotations. If someone has a better solution, I'm open to it.