PlusCal (anteriormente llamado + CAL ) es un lenguaje de especificación formal creado por Leslie Lamport , que se transpila a TLA + . En contraste con el enfoque orientado a la acción de TLA + en sistemas distribuidos , PlusCal se parece más a un lenguaje de programación imperativo y es más adecuado para especificar algoritmos secuenciales . [1] PlusCal fue diseñado para reemplazar el pseudocódigo , conservando su simplicidad mientras proporciona un lenguaje formalmente definido y verificable. [2] Un reloj de un bit está escrito en PlusCal de la siguiente manera: