プログラム仕様(1)

「仕様」。はてなのキーワードで見ると色々かいてありますがw 上二つのことですよ。そっから下にならないために、「仕様」というのを考えていきます。
 私の持つソフトウェア工学のうすーい知識だと、「こういう風に決めれば上手くいく」(フレームワークデザパタ)とか、「こうやって書けばわかりやすい」(UML)とかばかりが論じられていて、「そもそも仕様ってどういうもの?」ということが、欠けてると思うわけでして、そこら辺を今回は書こうかと思います。

さて、前回書いたように、「仕様」というものをソフトウェア工学でない見方をします。工学の立場的対義語は? 科学ですねw なので、ソフトウェア科学的な見方をします。

おそらくほとんどの人が知らないと思いますが、「プログラム」にも基礎理論が存在します。それを研究してるのが「ソフトウェア科学」です。
 では、「プログラム」は一体に何を拠り所にしているのかというと、「数学」です。微積と言った解析系ではなく、代数などの論理系の数学を基礎としています。この辺が、物質とか機械とかのいわゆる工学系と情報が一線を画すところですね。
 というわけで、「プログラム仕様」というものを、「数学の言葉」で書き換えたいと思います。

まずは、「数学の言葉」を考えましょう。
 例えば、「三角関数」という数学分野があります。

  • 目的
    • 「円を角度によって代数的に取り扱う」
  • 定義
    • 二次元平面の単位円上にある一点を取り、原点とその点を通る直線の角度をθとした時、その点のx座標をcosθ、そのy座標をsinθ、とする
  • 定理
    • cos2θ+sin2θ=1
    • 加法定理
    • etc.

という風に、「三角関数」という数学分野は考えられて行きます。なお、こういう数学分野のことを、「計算体系」と呼びます。
 まぁ、数学に慣れてないうちは、定義だとか定理だというのが良く分からなくて、かなり混乱したものですw
 混乱する理由は簡単で「定義」ということがよくわからないわけです。大抵は「定義」というのは「決まり事」なのだから、そういうものだと思え、と言われるわけですが、実はちょっと違います。
 なぜなら、計算体系を語る上でもっとも大切なことがあるからです。それが、一番上に書いた「目的」です。
 数学というと、基本的に与えられるものなので、かなり忘れがちなのですが、数学といえど、人の作ったものです。ということは、それを作る上での「意志」というのが、必ず内在してます。計算体系というのは、その「意志」を実現するために存在します。

その「意志」を、数学という言葉で記述するために作られる"最初の言葉"が「定義」です。
 そして、「定理」というのは、その"最初の言葉"を組み合わせて作られる"新しい言葉"ということになります。もちろん、"新しい言葉"と"新しい言葉"を組み合わせて、また別の"新しい言葉"を作ることはできます。
 但し、"新しい言葉"を作る上でのルールを忘れると、体系に矛盾が生じます。そのルールとは、その「定理」より「上の定理」しか組み合わせてはいけないということです。

論理に慣れてる人は、そんなの当たり前やん、とお思いでしょうが、思ってるより忘れてます。
 どういうことかと言いますと、計算体系はその中で階層構造を成しています。

体系の階層構造
目的
定義1 定義2 …… 定義n
第一定理1 第一定理2 …… 第一定理n
第二定理1 第二定理2 …… 第二定理n
以下続く
 例えば「第一定理1」を作る、つまり"証明"するには、それより上である「定義」の階層しか使ってはいけないわけです。同じ階層にある「第一定理2」ですとか、下の階層である「第二定理n」とかは、その証明には使ってはいけません。
 もし、使えてしまったら、その証明が間違っているか、その定理の在るべき階層が違うか、体系そのものが間違っているかの、いずれかです。

 また、「計算体系」がどのような性質を持っているか、ということを示す「計算体系」も存在します。「環」だとか「群」だとか「体」だとか、あの辺の話です。
 そういう体系を、ソフトウェア科学では「メタ」な計算体系と呼びます。これはちょっと話が逸れんですが、「プログラム」につなげるために重要な話なので、書いておきます。

 さて、じゃあ、「プログラム」はどうなのよ? って話ですが、眠くなってきたのでw それは明日というこで。