Recent content on John Senneker's blog
In our board representation we took some pragmatic shortcuts, constraining allowed boards more than was strictly necessary. However, we would still like to state winnability in the most general and abstract way we can. Essentially we would like to say that at any point in a Snakes and Ladders game, it is possible for someone to win the game. Before we can state this theorem, we need two new…
In the third post in this series, we will refine the abstract model we created in part 1 using the board representation we defined in part 2 . Recall the model BoardGame we established in the first post. There’s nothing specific to Snakes and Ladders in it; the same machine could be used as the base for most board games. To turn this into a Snakes and Ladders game, we need to add dice rolls…
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. Recall that a Snakes and Ladders board is a…
Recently I’ve been learning Verus , which is a system for proving the correctness of Rust programs. I’m particularly interested in defining abstract state machines in the style of TLA+ or Event-B , and using Verus to prove properties about those machines, as well as code implementing them. Event-B’s philosophy is to model your program with a simple abstract model first, and…
Recently I went to a park that had a brick labyrinth in it. The labyrinth comprised about 100 concentric rings of bricks. Here’s a picture of it taken from above:
John Senneker’s blog.