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

Recursive Array Update #92

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following fails:

type Buffer is ({int[] data, int wp} this)

assert:
  forall(Buffer[] xs, Buffer[] ys):
     if:
        xs == ys[0:=xs[0]{wp:=0}]
     then:
        xs[0].wp == 0

Presumably the reason is because the definition of xs is recursive. Certainly, if we swap it around so ys is being assigned then it passes:

type Buffer is ({int[] data, int wp} this)

assert:
  forall(Buffer[] xs, Buffer[] ys):
     if:
        ys == xs[0:=xs[0]{wp:=0}]
     then:
        ys[0].wp == 0