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 With ArrIdx_I #129

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following does not verify:

assert:
  forall(int i, int[] xs):
     if:
        xs[i] > 0
     then:
        (i >= 0) && (i < |xs|)

The problem is the term i < |xs|.