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

Another Bug with Flow Typing #83

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

(this maybe related to #77)

The following fails to type check:

define f_loopinvariant_15(int[] str, null|(int[]) r) is:
    (r == null) || (|r| == |str|)

The error message reported is expected array type on |r|.

DavePearce commented 7 years ago

UPDATE: this is because of r == null not being r is null which is really a verification condition generator bug. See here:

https://github.com/Whiley/WhileyCompiler/issues/712