Skip to content
Demonstrates using generative testing to find counterexamples of a simple theorem from *Certified Programming with Dependent Types*
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Negb.xcodeproj
NegbTests
LICENSE
README.md

README.md

This is a translation of the negb_inverse theorem from Certified Programming with Dependent Types into Swift.

Since Swift is not a proof assistant, the theorem is rendered as a generative test using SwiftCheck. For build-and-test convenience, a static snapshot of SwiftCheck is packaged with the project.

The test cases also demonstrate how generative testing quickly finds the error in a corrupted version of negb (Boolean negation) that always returns true.

This repository accompanies an exploration of this in light of a blog post.

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.