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

Preexisting Bug 2 #136

Closed DavePearce closed 6 years ago

DavePearce commented 6 years ago

(see also #86)

This program is generating the dreaded need to fix this preexisting bug error:

function double(int n) -> (int m):
  assume n >= 0
  int i = 0
  m = 0
  while i < n where m==2*i:
    i = i+1
    m = m+2
  return m

At a minimum, we need a proper error message to be reported.