このラボにライセンスは必要ですか。

いいえ。Z3 は MIT、SPIN は BSD、TLA+ のツールは MIT、Alloy は Apache 2.0 で、jar の中のソルバーはそれぞれのオープンなライセンスです。生徒の VM の起動時にインストールされ、私たちがそれらを配布することはありません。

アカウントのない生徒でもできますか。

パート 1 と 2、つまり Z3 と SPIN はできます。アカウントのない VM は Ubuntu のアーカイブにしか届かないので、TLA+ と Alloy はそこではダウンロードできません。サインインした生徒の VM は GitHub に届き、4 つとも入ります。

生徒は何かを壊せますか。

壊せるのは自分のコピーだけです。ツールはモデルを検査するだけで、他人のものは何も実行しません。生徒がファイルを壊しても、元のコピーが /usr/share/formallab にあります。

ラボは実際の生徒の VM でテストしましたか。

setup、レッスンのコマンド、チェックは、VM の代わりのコンテナ内の本物の Ubuntu 26.04 で実行し、チェックが各パートのあらゆるごまかしで不合格になり、模範解答で合格することを確認しました。実際に起動した生徒の VM と、プラットフォームのプロキシ越しのダウンロードは、授業の前に一度試す価値があります。

形式手法のラボ：1 つの VM で Z3、SPIN、TLA+、Alloy

このラボは、生徒一人ひとりに 1 台の Ubuntu VM と 4 つの検証ツールを渡します。テストは、試したケースで設計が動くことを示します。形式手法は、機械にすべてのケースを調べさせ、性質を証明するか反例を返させます。生徒は、ソルバーの Z3、Promela のモデル検査器 SPIN、検査器 TLC を持つ TLA+、そして Alloy を、それぞれ小さな問題で使います。

生徒のパソコンには何もインストールしません。ツールは本物で、ラボの README には問題が書かれていて、答えは書かれていません。

生徒が学ぶこと

設計を試すのではなく検証するとはどういうことかを、4 つのパートで学びます。Z3 では、試験の時間割のルールと、ルールから成り立つ主張を書き、その反対に解がないことを Z3 が見つけて証明します。SPIN では、2 つのプロセスの競合をトレースの中に見つけ、エラーが残らないようにロックを書きます。TLA+ では、ロックが何のためにあるかを表す不変条件を書き、ロックしないロックに対して TLC が出力する反例を読み、直します。Alloy では、人と友人関係として描かれた反例を読み、新しい事実を加えてモデルを直します。

ブラウザで動かす

VM ラボは、モジュールのラボタスクとして設定し、サンプルはラボのページにあります。マシンは小さく、CPU 1 つ、メモリ 1 GB、ディスク 10 GB です。Java のツールはそれぞれ 128 MB に制限され、全体が余裕で収まります。Z3 と SPIN は Ubuntu のアーカイブだけで足ります。TLA+ と Alloy は GitHub からダウンロードしますが、アカウントなしのゲスト VM は GitHub に届かないため、この 2 つのパートにはサインインした VM が必要です。

ラボを追加する. 担当するモジュールでタスクを追加し、Ubuntu VM ラボのカードを選びます。ページには compose ファイルの代わりにマシンの短い説明が表示されます。
サンプルから始める. ページには、そのまま使えるラボが用意されています。Formal methods を選びます。サンプルを使うと本文が置き換わり、元に戻すで自分の内容が戻ります。
公開して自分用のコピーを起動する. 公開してから起動します。ラボの setup スクリプトが、VM の初回起動時に Ubuntu のアーカイブから Z3、SPIN、Java の実行環境を入れ、TLA+ と Alloy を GitHub のリリースからダウンロードして、ファイルごとに決まったチェックサムで検証します。数分かかります。
ターミナルを開く. ターミナルを開き、ホームフォルダの README.md を読みます。4 つのパートでやることが書かれていて、答えは書かれていません。

このラボの基本レッスン

Formal Methods Basics は、Ubuntu VM であるこのラボで進める小さなレッスンです。導入、「できる」で書く目標、キーワード、スターター、考えごとの後の確認、よくある間違い、最後の確認があり、各ステップには実行ボタンがあって、そのコマンドをマシンのターミナルに入力します。生徒は、Z3 に答えられる質問と答えられない質問をし、ラボのモデルの競合を SPIN に見つけさせて再生し、正しいロックには成り立たない不変条件に対して TLC が出力する反例を読み、Alloy のインスタンスを見ます。

レッスンは見て回るだけで、ラボ本来のタスクは生徒に任せるので、答えは渡しません。

採点のしくみ

ラボにはチェックがあり、信じるのはツールだけで、生徒自身の言葉は信じません。Z3 自身が生徒の時間割のルールと README のルールを比べるので、手書きの答えや足りないルールは不合格になり、主張はルールから導かれ、ルールなしでは成り立たないものでなければなりません。SPIN は生徒のロックをチェック側の枠組みの中で実行し、ロックは枠組みのものをいっさい名指しできません。TLC は直したロックを、チェック側の不変条件と生徒の不変条件の両方で実行し、両方のプロセスが入れることが必要で、生徒の不変条件は付属の壊れたロックに破られなければなりません。そのため TRUE の不変条件は不合格です。Alloy は生徒のモデルを自分のファイルから開き、自分のアサーションを調べます。アサーションは成り立つ必要があり、友人の集まりを見つける実行も成功しなければなりません。出力の最初の行が理由を示します。

配る. 他のタスクと同じようにラボを割り当てます。希望すれば提出期限も付けられます。生徒にはそれぞれ専用の VM が渡され、アカウントがあればセッションの間も保存されます。
チェックを実行する. クラス一覧の生徒の行で「チェックを実行」を押します。保存された生徒のマシンのコピーを起動し (保存し直されません)、ラボのチェックスクリプトを root で実行して、合格したか、何が出力されたか、いつ実行したかを表示します。結果は生徒には伝わりません。
採点する. チェックが出力した最初の行を読みます。パートの名前と、何が足りないかが書かれています。たとえば Z3 が見つけた足りないルール、SPIN がまだエラーを見つけるロック、壊れたロックを捉えない不変条件、反例が残ったままのモデルなどです。もっと必要なら、理由を付けて作業を戻します。

GitHub の定義ファイル

このファイルがラボの定義のすべてで、プラットフォームが実行する文面そのものです。サイズ、setup スクリプト、補助コマンド、README、チェックが入っています。コピーして問題を変えれば、もっと長いラボが作れます。

このラボを試す、そして費用

無料の個人アカウントで、このラボの基本レッスンに取り組めます。毎月、ほとんどのレッスンに足りる無料クレジットがあり、カードは要りません。クラスで使う場合、学校は最初の365日間、生徒50人まで無料で、その後は生徒1人あたりの年額です。すべてのラボが含まれ、教職員は無料です。

よくある質問

このラボにライセンスは必要ですか。: いいえ。Z3 は MIT、SPIN は BSD、TLA+ のツールは MIT、Alloy は Apache 2.0 で、jar の中のソルバーはそれぞれのオープンなライセンスです。生徒の VM の起動時にインストールされ、私たちがそれらを配布することはありません。
アカウントのない生徒でもできますか。: パート 1 と 2、つまり Z3 と SPIN はできます。アカウントのない VM は Ubuntu のアーカイブにしか届かないので、TLA+ と Alloy はそこではダウンロードできません。サインインした生徒の VM は GitHub に届き、4 つとも入ります。
生徒は何かを壊せますか。: 壊せるのは自分のコピーだけです。ツールはモデルを検査するだけで、他人のものは何も実行しません。生徒がファイルを壊しても、元のコピーが /usr/share/formallab にあります。
ラボは実際の生徒の VM でテストしましたか。: setup、レッスンのコマンド、チェックは、VM の代わりのコンテナ内の本物の Ubuntu 26.04 で実行し、チェックが各パートのあらゆるごまかしで不合格になり、模範解答で合格することを確認しました。実際に起動した生徒の VM と、プラットフォームのプロキシ越しのダウンロードは、授業の前に一度試す価値があります。

無料アカウントを作成して、すべてのラボを実行しましょう。