Model Base
最終更新：
modelbase
コンテンツ
形式手法の独学
独学の道筋
職場で形式手法(主にAlloy)の話をするとそれなりに興味の反応はあるのものだが、 いざ初学者が形式手法を学ぼうかということになると、それは数学という名の城壁で 囲まれた難攻不落な要塞のような印象を持たれてしまう。 自分も先人の語りを聴いて形式手法に興味を持ったものの、一方でそれは到底手に余る 代物と敬遠する気持ちが強かった。数学の知識が余りにも乏しかった ことが物怖じの原因だったと思う。
最初に話を聞いてから約1年が過ぎた頃、職場の有志で命題論理を学習し 始めたのが独学の入り口となった。 当時は命題論理のような"地味"な勉強は基礎固めの為とわかっていても、 やはりその後にどのように知識の連鎖の果てに形式手法のツールの理解へと 導かれるのか、その道筋が想像ができずに学習意欲が減退したことを覚えている。
ということで現時点(2013年1月時点)の個人的な見解ではあるが、形式手法の独学の道筋をPFD(Process Flow Diagram)という成果物とプロセスの連鎖を表現する図解を使って紹介してみたい(PFDの簡単な説明は下記参照)。 形式手法に興味を持っているが、何からどう勉強(練習)しようかその手がかりを探している方への参考情報となれば幸いに思う。
PFD Process Flow Diagram について
PFDはコンサルタントの清水吉男先生から2005年に教えていただいた図式で、
チュートリアルも公開されている。PFDはソフトウェアの開発段取を
可視化すること(自分は"作業段取の設計"と言っている)に利用できる。
PFDについて詳しくは、以下のURL参照してほしい。
http://homepage3.nifty.com/koha_hp/process/Proc.Index.html
PFDを一言で説明すると、「成果物とプロセスの連鎖を表現する図式」ということになる。
ここで言う成果物とは必ずしも文書やソースコードといった有形な
ものに限らず、経験、知識、判断といった類の無形の成果もその範疇に入る。
成果物は矩形で図示される。
またここで言うプロセスとは、成果物を生み出すための行動(ex. xx作業する、xxを考察する、
xxを練習する、など)を指す。プロセスは円形で図示される。
今回PFDのカラーシンタックスを自分なりにカスタマイズして運用する。 具体的には以下のように成果物の属性によって色分けした。
- 始端成果物(青): 着目しているPFDのスコープ内で所与の成果物
- 中間成果物(白): 着目しているPFDのスコープ内で生み出す成果物
- 終端成果物(赤): 着目しているPFDのスコープ内で最終的に生み出すことを目標としている成果物
また、下位階層を持つ(内部で下位のPFDが展開される)プロセスは黄色で示した。
Today: -
Yesterday: -
Alloy Analyzer
抽象によるソフトウェア設計／付録 A 練習問題 解答例
形式仕様記述ツールAlloy Analyzerの解説本「Software Abstractions」の邦訳「抽象によるソフトウェア設計－Alloyではじめる形式手法」が出版されたので、これを機会に書籍の付録にある練習問題に(興味のある箇所をつまみ食い的に)挑戦してみる。
Today: -
Yesterday: -
