Contracts with existential quantification

[pschanely]

Post conditions are expected to satisfy for all possible inputs. In logic tems, the condition is universally quantified over the function's inputs. You might find yourself wanting instead to existentially quantify - that is, to say that a post condition is satisfied for at least one input. (but needn't be satisfied for all inputs)

Typical design-by-contact systems don't have a way to express existential quantification. CrossHair doesn't have any direct support for this kind of condition either. Comment below with your use cases if this is important to you!

On a one-off basis, however, you can use CrossHair to answer such questions: just invert the post condition and expect crosshair to fail, producing an example input. If you like, that input can then be used to create a unit test.

[pschanely]

Note #165 (reply in thread) as a use case. As noted there, if you need universal quantification inside existential quantification (i.e. ∃ x ∀ y ...) CrossHair doesn't yet have a good way to help you.