search

typelift / SwiftCheck

QuickCheck for Swift
MIT License
1.41k stars 105 forks source link

Existential Quantification #43

Open CodaFi opened 9 years ago

CodaFi commented 9 years ago

Using the equivalence

∃ {x} . P x ≡ ¬ ∀ {x} . ¬ P x

Define the inverse of a property. From there, negate on the inside and outside and define existential quantification.

CodaFi commented 9 years ago

From there use

∃! {x} . P x ≡ (P x /\ ¬ ∃ {y} . (P y /\ y ≠ x))

For uniqueness.

CodaFi commented 9 years ago

So this says... We expectFailure on the property then expectFailure on each test case. Seems awfully wasteful. Must disable shrinking too while we're at it ('cause it doesn't make sense). Will have to bring back once.

CodaFi commented 9 years ago

What if...

Isn't this just (extensionally) the same as expectFailure on the outside. Then we let the shrinker loop search for a minimum passing value and map it back to success.