El ajedrez es un juego de estrategia que, aunque aparenta simplicidad, oculta un profundo sistema de reglas. El autor lo modela como un sistema concurrente específico donde la ejecución se entrelaza de forma estructurada: estrictamente por turnos, alternándose entre blanco y negro.
Para analizar este sistema, se introduce el concepto de invariantes, divididos en dos categorías principales:
Los INVARIANTES DE ESTADO son predicados sobre una configuración única del tablero. Entre ellos encontramos:
• TypeOK: verificación de que cada pieza ocupa el espacio correcto
• UnReyPorColor y AmbosReyesEnTablero: comprobaciones básicas de sanidad
• ParidadDelTurno: conecta dos variables, estableciendo que las blancas juegan en turnos pares y las negras en impares
• JugadorAnteriorNoEnJaque: establece que el jugador que acaba de mover no puede estar en jaque
• NoAmbosEnJaque: corolario que impide que ambos bandos estén en jaque simultáneamente
Los INVARIANTES DE TRANSICIÓN son predicados sobre pares estado-actual/estado-siguiente:
• ConteoDeMovimientosCreceEstrictamente y TurnoAlterna: cada paso incrementa el contador de movimientos
• ConteoDePiezasNoAumenta: prohíbe que aparezcan piezas de la nada
• UnaSolaCapturaPorMovimiento: máximo una pièce puede desaparecer por movimiento
• ExactamenteDosCasillasCambian: el movimiento básico cambia exactamente dos casillas (origen y destino)
Estas invariantes resultan útiles al agregar reglas complejas como el enroque, la captura al paso o la coronación de peones. Por ejemplo, ExactamenteDosCasillasCambian se viola con el enroque (cuatro casillas cambian) y ConteoDePiezasNoAumenta sobrevive a la coronación (el peón se transforma en reina manteniendo el conteo).
Este enfoque formal permite verificar la corrección de implementaciones de ajedrez y constituye un ejercicio valioso para comprender sistemas concurrentes en general.