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
Problem with Counterexample Generation + Nominal Types #131
type string is (int[] self)
assert "type invariant not satisfied":
forall(string|bool str):
str is string
The problem is that string is a nominal type which the interpreter does not handle correctly. Specifically, it always returns false for an expression of the form [x,y,z] is T where T is a nominal type of some kind.
The following assertion fails:
The problem is that
stringis a nominal type which the interpreter does not handle correctly. Specifically, it always returnsfalsefor an expression of the form[x,y,z] is TwhereTis a nominal type of some kind.