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 following fails to verify for reasons unknown:
type PieceKind is (int x) where (0 <= x) && (x <= 5)
type Piece is ({bool colour, Complex_Valid_1.PieceKind kind} this)
type Square is (null|Complex_Valid_1.Piece this)
type RowCol is (int x) where (x >= 0) && (x < 8)
type Pos is ({Complex_Valid_1.RowCol col, Complex_Valid_1.RowCol row} this)
type Row is (Complex_Valid_1.Square[] squares) where |squares| == 4
type Board is ({Complex_Valid_1.Row[] rows} $) where |$.rows| == 4
assert "type invariant not satisfied":
if:
true
then:
{rows: [
[{colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}],
[{colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}],
[{colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}],
[{colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}, {colour: false, kind: 0}]
]} is Complex_Valid_1.Board
The strange thing about this one is that it has the hallmarks of being related to the verification limit. That is, if we reduce the required dimensions of the board appropriately, say to 2x2, then it works fine. However, adjusting the limit parameter doesn't seem to make any difference ... ?
The following fails to verify for reasons unknown:
The strange thing about this one is that it has the hallmarks of being related to the verification limit. That is, if we reduce the required dimensions of the board appropriately, say to 2x2, then it works fine. However, adjusting the limit parameter doesn't seem to make any difference ... ?