mvcgenを使って命令的プログラムの検証をする
初めての検証済み命令的プログラム