13/09/13 23:21:23.48 .net
>>114
Wikipediaの「形式手法」で説明されているように、
形式手法にもレベルがあっていいじゃないかと
で、伝統的なZやVDMは重量級で、Alloyなど最近は軽量級が注目されている
Prologについては、(>>108で書いたように)純粋Prologの表現力と型付けの弱さという欠点が、
軽量な形式手法としても問題が多いと見る
ただし、これは形式手法としての問題点であって、プログラミング言語としての問題ではない
また、PrologにはDCGによるDSL(ドメイン記述言語)およびメタインタプリタの開発に
適しているという、優れた特性がある
これを活かし、あるドメインに特化した軽量仕様記述言語と処理系を開発すれば、
先に述べた欠点を補うことができると思う
以下は、Prologで過去に開発した仕様記述言語で、2進カウンタを記述している：
process binCounter(ins:in, outs:out, carry:out).
state 0.
from 0,
when ins$0, output (outs$0, carry$0), to 0.
when ins$1, output (outs$1, carry$0), to 1.
from 1,
when ins$0, output (outs$1, carry$0), to 1.
when ins$1, output (outs$0, carry$1), to 0.
言語は通信プロトコルの仕様記述言語である Estelle を参考にしたステートマシンをモデルとし、
シミュレーション(=模倣)による振る舞いの確認が可能
最終的にはペトリネットへ変換して検証する予定だったけど、着手できぬまま放置している