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.
They way that tuples are handled in the verifier is proving somewhat problematic. In particular, the distinction (or lack thereof) between braces and tuples is a problem. The following is cut down from RecordAssign_Valid_2 and illustrates the problem:
type rec1 is (int r0)
type rec2 is (rec1 r0)
assert:
forall (rec2 r):
r$2[0][0] == 1
The problem is that the type of r is int which is not expected. Some possible solutions to this:
Use a different notation for tuples (i.e. not ()). Perhaps { and }?
Extend array types to be able to support tuples as well. For example, [int,int] is a pair of int whereas [bool,int*] is an array whose first element is bool followed by zero of more int elements.
Another aspect of this is to consider why we are so flexible with braces? One answer to this is that it helps delimit the pattern matching syntax I use.
They way that tuples are handled in the verifier is proving somewhat problematic. In particular, the distinction (or lack thereof) between braces and tuples is a problem. The following is cut down from
RecordAssign_Valid_2and illustrates the problem:type rec1 is (int r0) type rec2 is (rec1 r0) assert: forall (rec2 r): r$2[0][0] == 1The problem is that the type of
risintwhich is not expected. Some possible solutions to this:()). Perhaps{and}?[int,int]is a pair ofintwhereas[bool,int*]is an array whose first element isboolfollowed by zero of moreintelements.Another aspect of this is to consider why we are so flexible with braces? One answer to this is that it helps delimit the pattern matching syntax I use.