Шахматы — хитрый concurrent system c перемежающимся выполнением: белые, потом чёрные, потом снова белые. Автор предлагает смоделировать эту систему и вывести инварианты — условия, которые всегда должны выполняться. Сначала идут State invariants — предикаты над одним состоянием. TypeOK проверяет, что все переменные живут в правильных типах (скучно, но отлавливает кучу багов). OneKingPerColor и BothKingsOnBoard — базовые проверки. TurnParity связывает два состояния: белые ходят на чётных ходах, чёрные на нечётных. PreviousPlayerNotInCheck переформулирует правило «ты должен закончить ход не в шахе» как «посмотри назад: игрок, который только что походил, не в шахе». NotBothInCheck — следствие.
Потом идут Transition invariants — предикаты над парой <state, next-state>. MoveCountStrictlyIncreases и TurnAlternates следят, чтобы счётчик ходов рос, а цвета менялись. PieceCountNonIncreasing запрещает фигурам появляться из ниоткуда. SingleCapturePerMove уточняет: за ход исчезает не больше одной фигуры. ExactlyTwoSquaresChange — самое жёсткое: ровно две клетки меняют содержимое (источник пустеет, цель получает фигуру).
Автор замечает, что это модель только базовых правил. Интересно проверить, какие инварианты выживают после добавления рокировки, пешек, взятия на проходе. ExactlyTwoSquaresChange ломается: при рокировке меняются четыре клетки, при en passant — три (фигура убирается не с целевой клетки). PieceCountNonIncreasing переживает превращение пешки — количество фигур не меняется.
В конце комментарий James Corey: перечисление правил заставляет задуматься ещё до анализа. Оказывается, до XIX века не было ясно, что пешку нельзя превратить в короля, что могло удивить попыткой мата с ответом «Le roi est mort, vive le roi!».