クリーム色の背景、色付き表示、高コントラスト、大きな文字のほうが読みやすいですか？配色と文字を選ぶと、すべてのページに一度で反映されます。

無料モジュール

形式手法

形式手法を実際に動かして学びます。Z3、SPIN、TLA+、Alloy で、テストが見逃す誤りを全部の場合で調べ、反例を読めるようになります。

6件のレッスン315分のレッスン情報科学の中核

レッスン一覧

どのレッスンも全文を無料で読めます。無料アカウントを作ると、コマンドをラボで実行し、クイズと課題に取り組めます。

  1. 1 · 仮想マシンラボ

    テストだけでは不十分な理由

    テストが示すことと、証明が示すことを、言い分けられる。

    レッスンを読む

  2. 2 · 仮想マシンラボ

    ソルバーZ3で主張を証明する

    主張がいつも成り立つかを、Z3 に尋ねて読み取れる。

    レッスンを読む

  3. 3 · 仮想マシンラボ

    競合状態をモデルで見つける

    トレースを読んで、2つのプロセスの競合を見つけられる。

    レッスンを読む

  4. 4 · 仮想マシンラボ

    ロックを書いてSPINで検査する

    ロックを書いて、SPIN がエラーなしと報告するようにできる。

    レッスンを読む

  5. 5 · 仮想マシンラボ

    不変条件を書き反例を読む

    不変条件を書き、壊れたモデルの反例を読める。

    レッスンを読む

  6. 6 · 仮想マシンラボ

    Alloyで反例を読んで直す

    Alloy が示す反例を、集合と関係として読める。

    レッスンを読む

本物のラボで実習

このモジュールのレッスンは、あなた専用に起動するラボで実習します。使うラボ：

授業で使いますか？このモジュールを学生に割り当てると、教員用ガイド、自動採点つきの課題、学生ごとのラボを使えます。