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

Semantics for Arrays? #147

Open DavePearce opened 6 years ago

DavePearce commented 6 years ago

This is a cross-posting issue to raise awareness of this problem:

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

Specifically, that this assertion currently verifies:

assert "assertion failed":
    forall(int i):
        [][i] == 0

This is definitely relevant to #139.