形式的仕様記述

「UNISYS技報60号」より
要求仕様の形式的記述―Software技術はここに始まり，ここに窮まる―
http://www.unisys.co.jp/tec_info/tr60/60abs.htm#6005

某社の論文集で、前回課題７に取り組んだ時に見つけて中は見てなかったページ。関連の論文がいろいろ載っていて、読み始めると時間を忘れてしまう。特に上記のものは、まぁ今回の課題とはあまり関係ないのだが、実に深いソフトウェア技術の倫理？に関する考察が述べられている。最後の一節を引用させていただこう・・・

Bjo/rner の論文の標題が‘生き残るSoftware 産業’を謳っているのは,示唆的で あった.Software 技術者が工学的・科学的に裏付けられた職業的矜持を持たなけれ ば,産業としてのsoftware 開発の未来は無い.それは益々software への依存度を高 めざるを得ない,現代社会全体の未来をも,暗くするだろう.Weizsacker の著書に は,前節に引いた文章に先立って,次のような警句が有った:「我々のこの複雑な世 界を,できるだけ理論的に理解するよう促進するのを怠る者は,正に実践の場に於い ては,結局は利益よりも害を齎すことが多い」.

９９年の論文。
課題７に戻って、このテキストで参考文献とされている論文は８６年のもの。現役学生の頃の話なのか。そして、形式的仕様記述がどのレベルの概念なのか、標準的な記法があるのかもよくわからない。文献で述べられている記法と課題で参考にせよと示された例題でも記法が違い、何が使えるのかよくわからない。現在進行形な仕様記述言語としてはZ言語があるようだ。本屋や以前出入りしたソフトハウスさんの本棚でも背表紙は見たことがある。
今回の課題は、形式仕様記述する意味を考え、練習として一つ書いてみよう。記法の揺れは問題ではなくて、必要な記述が矛盾なく十分に行われているかが大事なのだろう。と解釈。そのような説明が欲しいもんだ。
さて、やるぞ。