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

Problem Asserting Boolean Variables #16

Closed DavePearce closed 8 years ago

DavePearce commented 8 years ago

The following fails with an internal failure:

assert:
    forall ([bool] xs):
        if:
            xs[0]
        then:
            xs[0]

In essence, there is no support for treating arbitrary expressions in this fashion. Instead, we currently need to rework the above as follows:

assert:
    forall ([bool] xs):
        if:
            xs[0] == true
        then:
            xs[0] == true

This will then correctly pass verification.

DavePearce commented 8 years ago

For now, I have put in a temporary fix for this.