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

Instantiating Array Assignments #55

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

In order to prove the following, we need to infer that xs = [a,b,c] from |xs| > 3

assert:
  forall (int[] xs):
    if:
      |xs| > 0
    then:
      exists (int v):
        xs[0] == v
DavePearce commented 7 years ago

This is related to #29.

DavePearce commented 7 years ago

Identical to #90. Closing.