search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Logical IFF #137

Closed DavePearce closed 6 years ago

DavePearce commented 6 years ago

Currently, the logical iff operator <==> is not supported. This previously wasn't a problem as WyC translated this into disjunctions for us. But, the latest version of WyC supports <==> all the way through. A simple example:

assert:
    forall(int x):
        (x > 0) <==> (x > 0)
DavePearce commented 6 years ago

Fixed.