Quint - 仕様に書いた失敗の順番は全部試し、書かなかった失敗は試さない
Quint は、システムが持つ状態と、状態を変える操作を書き、操作をどの順番で行っても守られるべき条件に違反しないかを機械に調べさせる仕様記述言語です。TLA+ と同じ Temporal Logic of Actions という論理の上に、プログラマーが読み書きしやすい型付きの文法と、仕様を実行して調べる CLI を載せています。 ...
Quint は、システムが持つ状態と、状態を変える操作を書き、操作をどの順番で行っても守られるべき条件に違反しないかを機械に調べさせる仕様記述言語です。TLA+ と同じ Temporal Logic of Actions という論理の上に、プログラマーが読み書きしやすい型付きの文法と、仕様を実行して調べる CLI を載せています。 ...