管理メニュー

Model Base

「形式手法の独学」のPFD

最終更新：

modelbase

- view
管理者のみ編集可

更新日2013-01-31
[ 形式手法の独学 ]

「形式手法の独学」のPFD

紹介するPFDは実際に自分が通った独学の道筋ではなく、 2013年1月時点で後進に相談されたらどのようにアドバイスするかの視点で書いたものだ。 また"形式手法"と一般的な表現を借りているが、ここではAlloyとSPINを背景とした技能習得に偏っている。

黄色いプロセスは以下のような下階層のPFDを持つ。

各プロセスの説明

P001_命題論理を学習する

  • 【なぜやるか】
    • 形式手法の全分野の基礎言語となるため。
    • 自然言語で考えることから離れて、記号システムの規則のみに従って推論する思考習慣を身に付けるため。
  • 【どのようにやるか】
    • 小学生の頃にやった計算ドリルのようにひたすら命題計算の問題を解き続け、違和感を払拭してしまう。
    • 計算問題は手を動かして解き、身体的な感覚を動員することで体得してしまう。
    • 含意の真理表は納得できなくても丸暗記する。
    • 公理と推論規則については疑問を抱かず無条件に受け入れる。それ以外(証明済みの定理は除く)は全てを疑うくらいの態度が良い。
    • "だいたい理解できた"と感じた程度でやめない。新しい思考習慣を定着させるために一ヶ月以上継続的に鍛錬する。
    • 先を急ぎたくなる気持ちは当然だがすべてはこの上に建てられる。以前は自明と思い込んでいたことや気にもとめなかったことについて、時間をかけて掘り下げて考える。

P002_述語論理を学習する

  • 【なぜやるか】
    • 形式手法の全分野の基礎言語となるため。
    • 事柄の性質や制約など(一般的に言うと"言明")を記号で表現する能力を得るため。
  • 【どのようにやるか】
    • 何が自由変数で何が束縛変数となりえるかを考えながら、日本語の言明を論理式に翻訳(和文数訳)してみる。
    • 一階述語論理だけフォーカスする(二階の述語論理は無視してよい)。
    • 教本によって記法が異なることがあるが、あまり気にしない。
    • 限量子に関する定理を使って述語計算する練習はあとまわしでも良い。
    • 必須でないが、「構造」「理論」「モデル」といった数学用語まで学んでみる (←これを学ぶとモデル発見器が何をするツールか気がつくことができる)。

P003_集合論_関係_順序を学習する

  • 【なぜやるか】
    • 形式手法の全分野の基礎概念であるため。
    • モデリングは考察対象を集合と関係で形式的に表現するため。
    • モノの並びや繋がりの性質を形式的に表現するため。
  • 【どのようにやるか】
    • おおまかには、集合→写像→2項関係→順序 の流れで学んでいく。
    • 単純な概念ばかりと甘くみて読み飛ばさないこと。できればひとつひとつの概念定義を述語論理に和文数訳しながら理解を定着させていく。
    • 外延性の公理など、自明なことを形式的に表現するセンスを味わっておく。
    • 2項関係の基本的な性質(反射律、推移律、対称律、反対称律、など)を述語論理で表現してみる。
    • 無限集合はやらなくてもよい。

P100_状態遷移システムの構成概念を理解する

  • 【なぜやるか】
    • 状態遷移システムとして仕様情報や設計情報を形式的に表現できるようになるため。
    • システムの振る舞いを定義する図式としてステートマシン図を利用できるようになるため。

P021_モデル発見器を学習する

  • 【なぜやるか】
    • Alloyを使った仕様記述の練習の準備のため。
  • 【どのようにやるか】
    • 形式手法の初心者がサンプルモデルだけを頼りに試行錯誤して習得できるツールではないので、最初は必ずチュートリアルに従ってみる。
    • 先入観を捨てること。例えば"extends"キーワードや"."演算子を見て自分が知っている(Javaなどの)プログラム言語の解釈で類推しようとする気持ちを捨てる。
    • Alloyに入力するモデルの記法と解析器の操作法を同時に少しづつ学んでいく。
    • "シグネチャ"を"集合"、"フィールド"を"関係"としてとらえる。
    • ドット演算子"."の使い方を重点的に学ぶ。
    • 述語論理で記述した言明をAlloyでどのように記述するか研究してみる。

P200_仕様の推敲を練習する

  • 【なぜやるか】
    • 対象システムの理解を形式的に表現する技術を習得するため。
    • 対象システムに潜む問題の有無を、人手を借りずレビューする技術を習得するため。

P004_時相論理を学習する

  • 【なぜやるか】
    • モデル検査器で検査する時制を含む性質には時相論理が使われるため。
  • 【どのようにやるか】
    • 2項関係の基本的性質と順序について復習しておく。
    • □と◇演算子の意味をクリプキ意味論で理解する。
    • 意味論を学ぶとき、"可能世界"などの哲学的な表現に出会っても気後れしないこと。
    • 線形時相論理(Linear Temporal Logic, LTL)に注力する。
    • どのような言明が時相論理で和文数訳できるか考えてみる。

P031_モデル検査器を学習する

  • 【なぜやるか】
    • SPINを使った設計検証の練習の準備のため。
  • 【どのようにやるか】
    • 形式手法の初心者がサンプルモデルだけを頼りに試行錯誤して習得できるツールではないので、最初は必ずチュートリアルに従ってみる。
    • この学習段階では非常に単純なモデルだけを使うこと。
    • Promelaの基本的な文法を把握するため単純なモデルを作り、シミュレーション実行でモデルを動かしてみる。
    • PANとよばれる検証器(C言語のコード)の生成法と検証器のコンパイル方法、そして検証器の実行方法を学ぶ。
    • "反例"とは何かを理解する。
    • assert, Endラベル、Progressラベルを使った検査を試してみる。
    • 検査したい性質をLTL式で表現し、実際にモデル検査してみる。
    • 反例のtrailを読み解いてみる。

P300_設計の検証を練習する

  • 【なぜやるか】
    • 試作するシステムが要件を満たすか否かを、人手を借りずレビューする技術を獲得するため。

P900_知見を整理する

  • 【なぜやるか】
    • 学習した技能を基点にして、より理解を深めるため
    • 実利的な適用を目指すことを考え始めるため
  • 【どのようにやるか】
    • 自分が理解したことを体系化して表現してみる、あるいは誰かに説明してみる。
    • 興味のあるシステム、製品、制度、アーキテクチャ、アルゴリズムなどについて形式手法で考察してみる。
    • 学んだことがどのような側面で実務に活かせるか検討してみる。
    • ある程度の無駄使いを覚悟でコンピュータサイエンス系の教本を乱読し、関心事や必要性を整理してみる。

各成果物の説明

I001_事例や業務経験

  • 【参考】
    Toyモデルを作るためのネタになりそうなもの。
    • 自動販売機など仕様を想像できそうな自動○○機の振る舞い
    • ○○サーバや○○クライアントなどネットワークシステムの振る舞い
    • スタックやキューなどのライブラリの振る舞い
    • Toyモデルにスケールダウンできそうな、業務で触れたシステムの要件／仕様／設計
    • 業務フローや作業手順
    • 制度やゲームなど特定の目的のもとに制定された規則

I002_数理論理学の教本

  • 【教本】
    ネットで検索すれば数理論理学の授業の教材が無料で手に入るのだが、主軸にする教材は出版物のほうが良いと思っている。ネットで手に入れた教材は授業を前提とした補完資料であったり、内容自体がまだ洗練されていない可能性もある。一方、元々は授業向けの教材だったしても書籍化された教材は、出版までに多くの労力が投入されており、著者以外の複数の識者によって監修/校正されているため一般的に質が高い。教本に投じるお金よりも学習に投じる時間のほうが馬鹿にならないので、ここはあまりケチらないほうが良いと思う。
    　
    数理論理学の教本はたくさんあり、難易度も学習目的もまちまちだ。何冊か投資して失敗してみるのも良い。ただし、高校の教科書程度のものや主題が別目的(例えばデジタル回路入門とか)で前菜のように数理論理学が紹介されているようもの、縦書きで数式があまり出てこない読み物系のものは避けたほうがよい。
    　
    また、数理論理学は数学基礎論という数学の基盤を整備する分野に属し、その分野では"証明"に対する徹底的な議論が展開される。そのため数理論理学の教本によっては公理系(公理と推論規則)の"健全性"や"完全性"といった公理系自身の妥当性を検証する議論に遭遇するが、それらは形式手法の習得に必須でないので無視してもかまわない（それらの議論に付き合うと精神的体力を消耗し、形式手法のツールを使うところまで辿り着けなくなってしまうかもしれない)。

  • コンピュータのための数学―論理的アプローチ-D-グリース
    根源的な説明からコンピュータサイエンスの基礎となるトピックが幅広く紹介されている良書。命題論理と述語論理の基礎学習が目的なら、やはりこの本がイチ押しに思える。公理、定理が豊富に紹介され端折りも少ない。演習も豊富だが解答は掲載されていない。
    残念なことにコンピュータサイエンス系の良書が絶版になることも度々(IT系の流行技術と違って簡単には陳腐化しないにもかかわらず！)で、2013/1時点でこの本の邦書は絶版になっている。コンピュータサイエンスの勉強を始めてみたい方は、多少予算オーバーでも中古品が見つかれば買ってしまうことを強くおすすめする。
  • 命題論理の学習
    "ライプニッツの規則"といった根本的なところから基礎固めするには第1章から学ぶのが望ましいが、少なくとも第2章、第3章はおさえる。第3章は等式論理での証明を中心にしており、他の教本のように自然演繹やシーケント計算での証明ではないが特に心配はいらない。
  • 述語論理の学習
    第8章、第9章をおさえる。特に第8章のように限量子だけに焦点を合わせて空制限域公理のような公理を紹介している教本(邦書)はめずらしい。述語論理を確実におさえるために第8章は貴重な情報源となる。

  • 論理学をつくる-戸田山-和久
    哲学者が書いたとても丁寧で紙面を多く使った説明が載っており初学者にとっての助けになる良書。自分は数理論理学の技術用語の理解の多くをこの本から得ることができた。入門書だが非古典論理までトピックを広げており、様相論理の学習までカバーできる。練習問題は多くないが巻末に解答が付いている。非常にお買い得な本なので絶版にならないうちに買いだめすることをおすすめしたい。
  • 命題論理の学習
    第1章～第3章までを読む。"論証とは何か"や"論証の正しさとは何か"と言ったような今まで考えたこともなかったことを学べる。
  • 述語論理の学習
    主教本は他の本にまかせ副読本として活用する。Alloyの使い方をある程度理解して簡単なモデリングができるようになった頃、この本の第5章～第7章までを熟読してみる。Alloyは何をするツールなのか、なぜモデル発見器と呼ばれるのか、そもそも"モデル"とは何なのか、などの答えを見出すことができる。
  • 数学は言葉―math-stories-新井-紀子
    ---述語論理の学習
    公理や定理で体系化した説明がないので個人的にこの本は主教本としては頼りないと思うが、副読本としてはかなり良い(一番かもしれない)。というのも、形式手法の独学で述語論理を学ぶ主な目的は言明を数学的に表現することであるが、この教本はその目的に非常に適している。言明を論理式に翻訳する作業である"和文数訳"という言葉はこの本で初めて知った。この本は和文数訳の例題が豊富に用意されている。本のタイトルの印象だけだと見逃してしまいそうだが、実は形式手法の初学者にはかなりのお役立ち本だと思っている。
  • 現代論理学〈1〉-マグロウヒル大学演習-John-Nolt
    自習用の教材としても作られており、練習問題が多く解答も掲載してある。他の教本に比べて数理論理学の専門用語の紹介が多くみられるが、今回の目的から考えるとそれらを覚える必要はない。巻末に"一人で学ぶ人へのアドバイス"というページがあり、多少参考になる。
  • 命題論理の学習
    自然演繹による証明である。第3章、第4章(反証図は飛ばしてOK)をおさえれば良い。
  • 述語論理の学習
    第5章、第6章(反証図は飛ばしてOK)をおさえれば良い。第5章はベン図を使って論理と集合のかかわりを学ぶので、形式手法の実践(集合を内包表現で記述するとき)に役立つ練習となる。
  • 論理学-野矢-茂樹
    数学の教本は基本的に 定義→定理→証明 の無機質な反復運動なので、飽きたり疲れてしまうこともある。この本は掛け合い談話で論理学の説明が進むので、読んでいて楽しい。それでいて練習問題もあり解答も掲載されている。数理論理学の勉強にちょっと疲れたけど、かと言って完全に休勉状態にするのは怖いな(もう勉強に戻ってこなくなる予感がする)と思うような場合に、こういった本でモードを変えてみるのもいいと思う。
  • 命題論理の学習
    第1章を読む。
  • 述語論理の学習
    第2章を読む(第1節は飛ばしてもOK)。

I003_離散数学の教本

  • 【教本】
    離散数学の教本はたくさん種類がある。内容もレベルもそんなにバラつきがないように思われるので相性がよさそうな本で良い。ただし目的は数学的構造を表現するための数学の語彙を増やすことなので、”冪集合”、”推移閉包”、”同値類”といった用語までカバーしているかどうかも教本選択の判断材料としたい。
  • 集合の学習
    第11章だけ読めばよい。第20章は無限集合のトピックなので無視してよい。この教本のように有限集合と無限集合のトピックを明確に分離してくれているのはありがたい。またこの教本全般に言えることなのだが、公理や定理を述語論理で示してくれているのはとてもありがたい。
  • 関係、順序の学習
    第14章だけ(P221までを)読めばよい。
  • 情報代数-情報数学講座-小野-寛晰
    入門書であるが説明に端折りがなく読みやすかった。この教本は公理や定理を述語論理で示していないので、後日Alloy言語で定理をモデリングしてみると良い。この教本は定義の端折りが無いので、ページを遡って読み返せば必ず定義が見つかるためモデリングに向いている。自分はこの教本の演習問題をAlloyでモデル化し、反例が生じないことをもって定理が理解できたと見なす自己トレーニングを実行してみたが、数学概念の正確な理解やモデルリングスキルの向上に非常に役立った。
  • 集合の学習
    第2章を読む。
  • 関係、順序の学習
    第3章を読む。順序についてはぜひとも辞書式順序まで読んでみることをお勧めする。
  • 独習コンピュータ科学基礎I-離散構造-James-L-Hein
    多分この説明を読んでいる人の多くはエンジニアであろう、そして数学の教本の 定義→定理→証明 の繰り返しに飽き飽きする人も多いのだろう。「独習コンピュータ科学基礎」のシリーズは証明を省いて例示が中心となっているのでエンジニアにはとっつきやすい教本かもしれない。そして演習問題の解答は出版社のWebサイトからダウンロードできるでありがたい。
    一方で、例示に傾倒する教本は概念の定義が曖昧に済まされ、なんとなくわかるが正確な概念把握に至れない危険もはらんでいる、と個人的には警戒感を持っている。ということでこの本は副教本としてお勧めする。
  • 集合の学習
    第1章 1.2 を読む。
  • 関係、順序の学習
    第4章 4.1～4.3 を読む。閉包については割と紙面を割いている。個々のアルゴリズムの説明について深入りする必要は無いと思う。

I004_様相論理を含む数理論理学の教本

  • 【教本】
    数学系の教本は様相論理が中心、工学系の教本は時相論理(推移律が成り立つクリプキフレームにフォーカスした様相論理の１つのインスタンス)が中心、という傾向がある。このPFDの狭義な目的からすればLTL式(線形時相論理 Linear Temporal Logic の論理式)で検証性質を書ければよい。したがって手っ取り早く済ませるためにはモデル検査器系の教本を読めばその辺りの情報は得られるのだが、自分の経験では様相論理の知識(特に、クリプキ意味論)を知らないと、時制表現が複雑なLTL式が書けなくなるので、様相論理から学ぶことをお勧めしたい。
  • [[論理学をつくる-戸田山-和久>http://www.amazon.co.jp/論理学をつくる-戸田山-和久/dp/4815803900/]] ⇒ 寸評はこちら

  • 様相論理の学習
    様相論理については第4章でしっかり書いてあるのでこの章をおさえる。章の後半に時相論理やそれ以外の様相論理の応用に簡単にだが言及されていて興味深い。
  • 言語・知識・信念の論理-知の科学-東条-敏
    様相論理を議論の中心に置いた人工知能系の入門書。個人的には非常に興味がそそられる内容だ。
    • 様相論理の学習
      "2章 可能世界の論理"と"3章 時間の論理"を読む。この教本では様相論理を"時制"の表現に適用することが説明の目的なので、モデル検査系の教本が取り上げる時相論理(LTLやCTL)は紹介されない。しかし時制表現を論理式として表すことを学べるので、この教本で得られるものは少なくない。なお、英語の時制表現を論理式に翻訳している例も載っており興味深い。
  • 様相論理の学習
    4.1.10で時相論理による性質記述を説明している。
  • Logic-Computer-Science-Modelling-Reasoning
    洋書の紹介。
    時相論理が学べる洋書の中でこの本が優れているということではなく、この本が、命題論理、述語論理、時相論理(LTL,CTL)、プログラム検証など形式手法の広範囲のトピックに触れており、さらにはAlloyの解析器エンジンであるSATソルバについも触れているのがお勧めの理由。
    • 様相論理の学習
      LTL(線形時相論理)については 3 Verification by model checking　の 3.2 Linear-time temporal logic を読む。 いちよ様相論理の学習は 5 Modal logics and agents を読むことで可能だが、その部分については他の教本のほうが良いと思う。

I005_モデル発見器_Alloy

  • 【Web】
    • Alloyのダウンロード
      2013/1時点の最新バージョンは4.2(4.2より古いバージョンは日本語が使えないので注意)

I006_Alloyのチュートリアル

  • 【教本】
    • 抽象によるソフトウェア設計-Alloyではじめる形式手法--Daniel-Jackson
      Alloyを学ぶなら必ず手元に置いておきたい本。
      まずは2章で全体観を養い、その後3章、4章を流して文法をおおまかにおさえる。5章で解析方法を学ぶ。一読してわからなことがあっても全然かまわない。実際にモデリングをする過程で何度も読み直せばよい。
      6章の事例に進むより、自分で簡単な例を作ってモデリングを繰り返してみるほうが習得が早いと思う。

I007_モデル検査器_SPIN

I008_SPINのチュートリアル(★未記載)

I901_形式手法のガイド

D001_命題論理の知識

  • 【何を得るか、どんな状況になるか】
    • 命題、論理式、公理、定理、推論規則、トートロジー、充足可能、同値　などの用語を説明できる。
    • 含意記号を日本語の"ならば"と混同しなくなっている。
    • (P⇒Q) ≡ (￢P∨Q) や (P≡Q) ≡ ( (P⇒Q)∧(Q⇒P) ) 　などが常識になっている。
    • その気になれば論理和や論理積についての以下のトートロジーを証明する自信がある。
      • 冪等律、結合律、交換律、吸収律、分配律、ド・モルガンの法則
    • 命題論理に公理系が複数あることを知っている。

D002_述語論理の知識

  • 【何を得るか、どんな状況になるか】
    • 議論領域(論議領域、対象領域などとも呼ばれる)、自由変数、束縛変数、などの用語を説明できる。
    • それなりに和文数訳に自信がある。
    • 和文数訳が難しい和文のケースに心当たりがある。
    • 述語論理におけるド・モルガンの法則を理解している。
    • 限量子の制限域が空の場合に式の値がどうなるか(=空制限域公理)を知っている。

D003_数学的構造の知識

  • 【何を得るか、どんな状況になるか】
    • 内包表現で集合を記述できる
    • 単射、全射、直積、定義域、値域、関数、冪集合、推移閉包、反射律、推移律、対称律、反対称律、同値関係、同値類、半順序、全順序、極大値、最大値、上限、上界、などの用語を説明(もしくは述語論理で表現)できる。
    • 関数は直積集合の部分集合であるという考えが定着している。
    • 例えば"半順序関係"など、数学が定義を与えてる情報構造を一階述語論理に翻訳できること

D004_時相論理の知識

  • 【何を得るか、どんな状況になるか】
    • LTL式で「何か悪いことが決して起こらない」(安全性特性)、「何か良いことがいずれ起きる」(活性特性)を表現できる。
    • クリプキ意味論の立場から安全性特性や活性特性を表すLTL式の意味を説明できる。
    • 排他制御、応答性、進行性などの性質記述をLTL式で示せる。

D021_モデル発見器の利用知識

  • 【何を得るか、どんな状況になるか】
    • 解析対象の記述能力を培う
      • 一階述語論理で記した言明をAlloy言語に翻訳できること
      • 例えば"半順序関係"など、一階述語論理で記述できる情報構造をAlloy言語に翻訳できること
      • UMLのクラス図を使って表現したい情報をAlloy言語で表現できること
      • どのような制約記述で推移閉包を使うのか、感覚が得られていること
      • Alloyに同梱されているライブラリ util/relation のモデル記述を読んで理解できること
  • 解析結果の観察能力を培う
    • Viz表示の他、Tree表示やEvaluatorを活用して解析結果を調査できること
    • Themeを編集して着目点のわかりやすい解析結果に加工できること
    • 解析器が探索するスコープの変更ができること。

D031_モデル検査器の利用知識(★未記載)

  • 【何を得るか、どんな状況になるか】

D100_状態遷移システムを形式的に表現する知識

  • 【何を得るか、どんな状況になるか】
    • 状態遷移システムを数学的に把握できるようになる。
    • 仕様情報や設計情報を形式的に図式表現できるようになる。
    • システムの外部仕様と内部仕様を分別して表現できるようになる。

D200_仕様を推敲する技能

  • 【何を得るか、どんな状況になるか】
    • 思考習慣
      • 集合と関係で情報構造を捉える思考が培われ、物事を数学的に把握する習慣が身に付くこと
      • 考察対象の状態空間を明確にする習慣が身に付くこと
      • 積極的に不変条件を明確にする習慣が身に付くこと
      • 事後条件は事前と事後の状態間の差として捉える習慣が身に付くこと
  • 考察能力
    • 振る舞いの仕様をプロトコルステートマシンとして把握できること
    • 着目したい事柄には不要な情報を形式化の際に捨象できること
  • 運用技術
    • 解析器がインスタンスを発見しない場合、制約条件を調整して効率的に仕様記述のバグを探せること
    • 問題領域を階層化し形式記述をmodule分けできること

D300_設計を検証する技能(★未記載)

  • 【何を得るか、どんな状況になるか】

D900_形式手法の技能向上の基盤

  • 【何を得るか、どんな状況になるか】
    • 思考体質が強化される
      • "形式"に従うことで、前提条件とそこから導いた結論に対して明快に説明できるようになる。
      • 数学の語彙や概念を使って解釈を得る思考習慣が育まれ、考察対象に対する曖昧さの認識が的確になる。
      • 考察対象の中から関心事以外を捨象する能力が向上する。
  • 業務における形式手法の適用を考察できるようになる
    • どのフェーズで、どの対象について、何を得るため、どういうメンバーで、どのような具体的な作業として適用するのか、ということを自分なりに考察できるようになる。
    • 従来の開発作業を思い返し、それらの作業断片は結局のところ形式手法のアプローチでいうところの、何を明らかにする思考作業だったのか自問自答できるようになる。
  • その他の形式手法の学習が比較的容易になっている
    • 証明によりプログラムを検証する技術を学習する知識基盤が得られる。
    • プロセス代数により並行システムを検証する技術を学習する知識基盤が得られる。 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　 　
「「形式手法の独学」のPFD」をウィキ内検索
記事メニュー
最近更新されたページ
もっと見る
目安箱バナー