「SPINモデル検査」第1回(5月10日)

Posted on by 1 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 pp. i – 6

序文

まえがき

  • SPINとは
  • SPINとの出会い
  • 本書の特徴
    • p. v 本節下から2行目
      パソコンにインスールして → パソコンにインスールして
  • 本書の構成と読み方のガイド
    • p. v 第2章 見出しの最後
      使い方 → 使い方
    • p. v 下から2行目
      「反駁」の読み方は? → はんばく
  • SPINの入手法
  • 謝辞

目次

(まえがきに「本書の構成と読み方のガイド」があったので、読むのを省略)

第1章 モデル検査とは — 自動検査とモデル検査法

  • 1.1 振舞い仕様とモデル検査法
    • 1.1.1 振舞い仕様と状態遷移システム
    • 1.1.2 状態空間の網羅的な探索
      • p. 5 図1.3
        copyやpr.putなど、状態を表す○の真上に書かれているものがあるが、状態名を表しているのではなく、pr.getなどと同様、遷移のイベント。
      • p. 6 図1.4
        図1.3を合成して図1.4になることを確かめておこう。

One comment on “「SPINモデル検査」第1回(5月10日)

  1. 「SPINモデル検査」図1.3 → 図1.4

    「SPINモデル検査」1.1.2の図1.3を合成してみました。…

コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

CAPTCHA