PlusCal

PlusCal (旧称 +CAL) は、 Leslie Lamppost により考案された形式仕様言語で、 TLA⁺ に変換される。TLA⁺ のアクション志向が分散システムに重点を置いているのとは異なり、 PlusCalは逐次命令形のプログラミング言語と似ており、シーケンシャルアルゴリズムの記述により適している^[1]。PlusCalは  擬似コード を置き換えることを目的に設計されており、その簡潔性を維持する一方で形式的に定義され検証可能な言語を提供している^[2]。

例として、1ビットクロックはPlusCalでは次のようにかける。

-- fair algorithm OneBitClock {
  variable clock \in {0, 1};
  {
    while (TRUE) {
      if (b = 0)
        b := 1
      else 
        b := 0    
    }
  }
}

PlusCalのツールとドキュメントは PlusCalアルゴリズム言語のページ から参照することができる．