Modeling Snakes and Ladders: The Board (opens in new tab)

In the last post, we introduced Verus and used it to create an abstract formal model of Snakes and Ladders. The model knows that the board has some number of squares, that players take turns moving around the board, and if someone lands on the final square the game is over, but the board itself was abstracted away completely. Here, we model the board.