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.
The inclusion of a record update operator would help with the generation of verification conditions in the Whiley Compiler.
Overview
This operator would work in a roughly similar way as the existing array update operator. Here's an example:
type Buffer is {int[] data, int wp}
assert:
forall(Buffer x, Buffer y, int[] ys):
if:
x == y{data:=ys}
y.wp >= 0
then:
x.wp >= 0
Here, y{data:=ys} returns the record y with field data now updated to ys. Thus, for example, it follows that x.wp == y.wp, etc.
Syntax
An important question is what syntax to use. The existing syntax for arrays is arr[i:=v], and we want something to distinguish from this (otherwise parsing yields an abstract tree node, etc).
The inclusion of a record update operator would help with the generation of verification conditions in the Whiley Compiler.
Overview
This operator would work in a roughly similar way as the existing array update operator. Here's an example:
type Buffer is {int[] data, int wp} assert: forall(Buffer x, Buffer y, int[] ys): if: x == y{data:=ys} y.wp >= 0 then: x.wp >= 0Here,
y{data:=ys}returns the recordywith fielddatanow updated toys. Thus, for example, it follows thatx.wp == y.wp, etc.Syntax
An important question is what syntax to use. The existing syntax for arrays is
arr[i:=v], and we want something to distinguish from this (otherwise parsing yields an abstract tree node, etc).