dhrnameのブログ

プログラミング関連を語るよ

ダイクストラ不変量とクラスの抽象化 - 構造化プログラミングの覚え書き　その6

はじめに

目次

前回までのおさらい

　前回は、構造化プログラミングの「抽象化」の定義について見てきた。

データ構造化における抽象化の定義 - 構造化プログラミングにおける覚え書きその5 - dhrnameのブログ

ホーアによれば、抽象化は以下の4段階に分けられる。

  1. 抽出
  2. 表現
  3. 操作
  4. 公理化

　今回はダイクストラの「不変量」の概念を考えていこう。

記事の注意点

  • チャーチの提唱 (Church's Thesis)は「計算可能=再帰的」で非構造化
  • チャーチの定理 (Church's Theorim)は「無矛盾=決定不能」で構造化
  • 「オブジェクト (対象、object)」、「クラス (class)」、「サブクラス (部分クラス、subclass)」、「インスタンス (実例、instance)」、「this」、「new」は1972年版の書籍『構造化プログラミング』の定義に従う。かっこ内の訳は75年の日本語版*1訳者の武市正人氏による
  • 上記の注意点については一切質問や意見を受け付けない

　まず、不変量*2(invariant)とは数学用語あるいは物理学用語である。この「不変量」をプログラミングで用いたのは、ダイクストラ*3である。ヴィルトの考え方*4と区別するため、以下、この概念を「ダイクストラ不変量」、あるいは単に「不変量」と呼ぶ。

　ダイクストラ不変量は構造化プログラミングにおいてきわめて重要な原理である。前半ではダイクストラによる1972年版の書籍「構造化プログラミング」を取りあげ、後半ではクラスプログラミングでの応用を考えていく。

ダイクストラ・メッセージの構造化原理

ダイクストラが提唱したダイクストラ・メッセージ

　1965年に、ダイクストラは「メッセージ」(message)の概念をアメリカの研究誌「Communications of the ACM」上で提唱した*5。このメッセージの元になったのは数学者J.デッカーのアイデアである。

　このダイクストラ・メッセージは「連接」、「選択」、「繰り返し」の3パターンの制御で構成される。複数のプロセス同士で「お先にどうぞ」とメッセージをお互いにやりとりして、ゆずり合う。メッセージを発した方は待ち(待機、wait)の状態となり、待ち状態の間にメッセージを受けたら自身の処理を実行に移す。そして、自分の処理を終えると、再び「お先にどうぞ」と相手にメッセージを発して待ちの状態に入る。こうして、互いにメッセージを出してゆずり合いながら、共有メモリの相互排除問題を解決する。

　1966年に、ダイクストラは「協調逐次プロセス (Cooperating Sequential Process)」という講義をNATOの国際会議で行った。その会合の参加者には、ホーア(レコードクラスの提唱者）とダール(オブジェクトクラスの提唱者）もいた。

　その際、ダイクストラはダイクストラ・メッセージをNATOの会議で紹介した。ダイクストラはホーアとダールを含めた科学者たちの議論を経て、1972年、学者たちの論法と結び付けられる次のような原理を「構造化プログラミング」の本の中で発表した。

ダイクストラ・メッセージの構造化原理
  • 「数え上げの推論」--「連接」と「選択」
  • 「数学的帰納法」--「繰り返し」
  • 「抽象化」--「連接」と「選択」と「繰り返し」
  • 「数学者が無意識のうちに字形を変えているもの」-- 「抽象化=データ型」

　このダイクストラ・メッセージの構造化原理は一台の計算機ではなく、接続された二台以上の複数の物理的な機械と、二台以上の複数の仮想機械を前提としている。ただし、これらの物理的な機械は独立して動くものとする。

　この構造化原理で挙がった3パターンにこだわったコードを書けば、そのコードは型安全かつ、クリティカルセクション競合は起きない。それが大規模なソフトウェアの信頼性につながるのである。

手続き型プログラミングから構造化プログラミングへ

　1972年、ダイクストラたちは、手続き型プログラミングの問題点を整理した上で、構造化原理に関わる自分たちの研究成果を『構造化プログラミング』という一冊の本にまとめた。

  • ダイクストラの階層 (hierarchy)　（『構造化プログラミング』第一部で解説）
  • ヴィルトの段階的洗練 (step-wise refinement)　（第一部で解説）
  • ホーアのデータ構造化 (data structuring)　（『構造化プログラミング』第二部で解説）
  • ダールのオブジェクトクラス（対象クラス、Object Class) 　（『構造化プログラミング』第三部で解説）

以上の4つの技術はダイクストラ・メッセージ構造化原理の応用が可能である

　手続き型プログラミングの問題点はクラスプログラミングのところで述べる。

数え上げ(enumeration)の推論と連接と選択

　まず、逐次実行(順次処理)される計算について考えてみよう。文Aの後で文Bが実行されるとき、改行とセミコロンを用いて以下のような擬似コード*6を書ける。

A;
B;

このとき、AやBは文(言明、statement)であり、数式や論理式とは区別するようにする。

さらに、条件節として、次のようなif文の擬似コードを用いてみよう。

if (条件式) {
　　条件式が真である場合、この範囲の文が実行される
}

　このとき、if(...){...}で一つのまとまった文となる。

　こうして逐次実行される計算が最後まで機械により読み上げられるとき、その逐次実行される文を「数え上げ」(enumeration)の集合とみなす。ただし、記号==は等号「=」であり、等号=は代入、記号<=は「≦」（小なりイコール）、>=は「≧」（大なりイコール）であるとする。

不変性の証明に関する例題

さて、いま、変数 r と変数 dd に対して、次の二つの文が続けざまに実行されるとき、

dd = dd / 2;

if ( dd <= r) {

  r = r - dd;

}

次の関係式が不変量であることを証明せよ。

0 <= r < dd    (1)

この証明は以下の通りである。

ダイクストラの証明

(1)が成立すると仮定して、プログラムの最初の文「dd = dd/2」を実行すると、dd の値を2で割るが r の値は変えないので、関係式

0 <= r < 2*dd    (2)

が成り立つ。ここで、次の互いに排反的な2つの場合に分ける。

　(ア）　dd <= r の場合、(2)より、次の関係式が成り立つ

               dd <= r < 2*dd    (3)

        この場合、r からddを引くというif文の{..}内部が実行されるので、結局(3)から

              dd-dd <= r-dd < 2*dd-dd

              0 <= r < dd

        が成り立つ。すなわち、(1)が成り立つ。

  (イ)         non dd <= r (すなわち、dd > r )の場合、

        if文の{..}内部は実行されず飛ばされるので、r はそのまま最終的な値をとる。

        さらに、最初の文の実行後に成り立つ 「dd > r」より、ただちに、

              0 <= r < dd

        が導かれれるので、やはり(1)が成り立つ

よって、(ア)の場合でも(イ)の場合でもいずれも(1)が成り立つ。証明終了

注意点

　ただし、不変量が実際にあるにもかかわらず、プログラムの実行前、あるいは、実行の最中に不変量の関係式(1)が立ち現れることはない。すなわち、我々人間は不変量を認識する能力が不足しているのである。

数学的帰納法と繰り返し

　数学的帰納法はループや再帰的手続き( recursive prodedure)を扱える推論のパターンである。例を挙げていこう。

例題

　次のような値の列 diがあるとする。ただし、propは与えられた(計算可能な)条件式であり、Dはある特定の値であり、fは（計算可能な）関数である。代入と区別するため、等号「=」の代わりに記号==を使う。

    d0, d1, d2, d3...     (1)

    i == 0に対して、di == D     (2a)

    i > 0 に対して、di == f(di-1)    (2b)

 このとき、変数"d"に対して、次の関係式

    d == dk     (3)

が成り立つようにせよ。ただし、kは以下を満たす値として与えられる。

    式prop(dk)は真    (4)

    0 <= i < kである全てのiに対して、non prop(di)、すなわち、prop(di)は偽    (5)

ダイクストラの証明

　ここでwhile文は条件が成り立つかぎり{...}を反復する繰り返し節であるとする。

while (条件式) {

 　　条件式が真であるかぎり、この範囲の文が実行される（以降、繰り返される文）

}

　この繰り返し節は前の例題の条件節を用いて、次のように定義することが可能である。

while(B){S} :=

if (B) {

  　S;

  　while (B) { S; }

} (1.1)

　いま、つぎのようなプログラム(6)を考える。

d = D;

while ( non prop(d) ) {

    d = f(d);

}

　さて、このプログラム(6)において、つぎを証明したい。

繰り返される文がn回実行されたとき(n >= 0に対して)

  • d == dn     (7a)
  • 0 <= i < n となるすべてのiに対して、non prop (di)     (7b)

が成り立つ（8)

　まず、数え上げの推論により、上の命題(8)は、n == 0 に対して成り立つ。すなわち、関係式(7b)が成り立つのは 0 < n の場合のみだから、(7a)だけ考えればよい。

n == 0のとき、定義(1.1)より、

d = D;

if (non prop(d)) {

    d = di;

}

なのだから、

2aと(6)より

　　d == D == d0

　　d == d0

これで、n == 0の場合、命題(8)が成り立つことを示せた。(9)

続けて、n == N (N >=0)に対して命題(8)が成り立つとき、n == N + 1に対しても命題(8)が成り立つことを数え上げの推論で示したい。

　繰り返される文が第N回目で終了した時点で、関係式(7a)と(7b)がn == Nに対して成り立つと仮定する。

　第N+1回目が実行されたときのことを考えよう。このとき、必要十分条件として、

　　non prop(d)

が成り立つ。これは(7a)より、n == N (すなわち、d == dN)に対して、

　　non prop(dN)

の成立を意味する。よって、n == N + 1に対して、条件(7b)が成り立つ。(10)

　さらに、d == dNと(2b)より、

　　f(d) == dN+1

が成り立つ。

　そして、繰り返される文

　　"d = f(d)"

の第N+1回目の実行の結果として、関係式

　　d == dN+1

が成り立つ。すなわち、n = N + 1に対して、関係式(7a)が成り立つ。(11)

　よって、(9)、(10)、(11)と、帰納法により、命題(8)が証明された。

　ここで、プログラム(6)の繰り返し文をk回実行すれば繰り返しが終了することを示そう。n > kに対して、第 n 回目の実行が起きないことを示したい。もし、実行されれば、(7b)より、

     non prop(dk)

を意味することになり、これは(4)と矛盾する。繰り返される文の第 n 回目の実行後、繰り返しが終了するとき、終了するための必要十分条件

    non non(prop(d)

は、(7a)より、

    prop(dn)  (14)

となる。これにより、n < kでは、終了しないこととなる。というのは、そうでなければ、(5)に矛盾するからである。したがって、繰り返しは n == kで終了する*7。

　よって、(7a)より(3)が、(14)より(4)が、(7b)より(5)がそれぞれ導かれる。証明終了。

「連接」と「選択」と「繰り返し」の抽象化

連接と選択と繰り返しの正しさについて

　これまで見てきたように、二つの論法は、3パターンの制御「連接」、「選択」、「繰り返し」とのつながりがある。

  • 「数え上げの推論」ー「連接」と「選択」
  • 「数学的帰納法」ー「繰り返し」

　つまり、この3パターンを使ったコードは、そのまま、これら論法の正しさ(正当性、correctness)を主張できる。

手続き型プログラミングの問題点

　ところで、手続き型プログラミングで「連接」、「選択」、「繰り返し」の3パターンを実現するには、いくつかの問題点が存在する。特に、以下の疑似コードには、「連接」と「繰り返し」を実現するうえで大きな問題点が存在する。エラーが起きるコードの行頭に?を付けておく。

手続き型プログラミング

procedure P() {

?   own int x = 0;

    procedure m() {

           x = x + 12;

    }

?   P();

}

? P();

? x = 10;

? m();

　ALGOL60言語のown(所有)変数は静的変数である。手続きを呼び出すたびに前の値を持続して再利用できる。だが、ここでは手続きPが再帰呼び出しされているため、再利用が不可能なので、?を付けている。

　また、局所変数xとmがブロック内部に存在するため、外部で利用できないのは明らかである。それゆえ、「連接」において、x=10;とm();にはエラーが起きる。

　そこで、以下のようにクラスプログラミングの疑似コードを考えていこう。

クラスプログラミング

PClass:{

    int x = 0;

    procedure m() {

          x = x + 12;

    }

}

Ref(P) p = new PClass();

p.x = 10;

p.m();

　コードのPClassはクラスであり、変数pはインスタンスである。同様に、PClass内部の局所変数xがpを通じて持続的に生き続けている。また、.（ドット）を使ってxの再利用が可能である。

　以下のように再帰呼び出しによって手続きPの繰り返しが続く間、その局所変数 x はスタックに積み上げられて死なずに永続する。

procedure P() {

   int x = 0;

   P();

}

　この再帰呼び出しと同様に、インスタンスもまた、メモリに写像された計算停止不能な計算である。それゆえ、インスタンスは永続的に生き続けるクラス内部のブロックである。

　今までは制御文として複合文と、if文とwhile文を使ってきたけれど、今度は代わりにクラスプログラミングを使って「連接」、「選択」、「繰り返し」が実現できることを示そう。

クラスプログラミングの抽象化

ダイクストラ連接（継承）

　二つの連接しているブロックAとブロックBについて、A内部の入れ子にしている手続き(procedure) や変数を、外部のB内部でも活用できるとき、ブロック同士のダイクストラ連接(継承)と呼ぶことにする。

　たとえば、ブロック内部の局所変数xと手続きpを他のブロックでも扱いたい。このために、疑似コードを示そう。

　以下では、PrefixClassと名付けられたブロックとSubClassと名付けられたブロック同士がダイクストラ連接している。ただし、ダイクストラ連接はB < Aと書き、変数 x のデータ型 t の宣言はt xと書く。

PrefixClass:{

    int x = 0;

    procedure p() {

         x = x + 1;

    }

}

 

SubClass < PrefixClass:{

    int y = x-1;

    procedure q() {

         p();

    }

   q();

}

 

Ref(SubClass) obj = new SubClass();

　この一連のコードは、ブロック同士が連接しているわけだから、実際、

int x = 0;

procedure p(){...}

int y = x - 1;

procedure q() {p();}

q();

といった、かんたんな逐次処理である。これらPrefixClassやSubClassのようなブロック*8を「クラス(class)」と呼ぶ。ダール・オブジェクトクラスとしてSIMULA67(1967年リリース）に取り入れられた考えである。

　ブロック内部の局所変数は外部からはアクセスすることができない。したがって、局所変数xの有効範囲と無効範囲は、

PrefixClass:{

   xの有効範囲

}

xの無効範囲

SubClass < PrefixClass:{

   x の有効範囲

}

xの無効範囲

Ref(SubClass) obj = new SubClass();

となって、PrefixClassとSubClassは数珠つなぎとなる。

　また、クラスの連接（継承）は証明そのものと深い関連がある。すなわち、数学者が一つの定理を詳しく証明するのに補題を示すように、プログラマは一つのクラスを詳しく述べるのに連接でつなげたサブクラス（部分クラス）を使う。

　この連接・継承の技法を広く世に知らしめたのは、SIMULA67言語とそれを解説した1972年版の「構造化プログラミング」である。

ダイクストラ選択（選出）

  クラスプログラミングでは、「カルテシアン積*9のダイクストラ選択(選出)」も可能となる。次のようなPrefixClassクラスがあったとする。

PrefixClass:{

    int x = 0;

    int y = 0;

    procedure p() {

         x = x + 1;

    }

}

このとき、インスタンス変数objに.(ドット)を使って、{...}内部にアクセスできる。

Ref(PrefixClass) obj = PrefixClass();

obj.x = 12;

obj.p();

このobjは直積 int × int × procedure*10であり、obj.xはその射影である。データ型を集合とみなして整理すると、

obj.x: int × int × procedure -> int

obj.x∊int

である。obj.xはいくつかのデータ型からint型を選出し、int集合から12という値を選出しているのである。それゆえ、obj.x = 12;のような代入を「選択的更新(selective update)」と呼ぶ。

　このことは、次のように連接したSubClassクラスでも成り立つ。以下では、SubClassから生成したobj2でも.xや.p()が使えることを示している。

SubClass < PrefixClass:{

    int y = x-1;

    procedure q() {

         p();

    }

}

 

Ref(SubClass) obj2 = new SubClass();

obj2.x = 12;

obj2.p();

ダイクストラ繰り返し（再帰データ型）

　クラスを用いて再帰データ型を考えてみよう。Ref(T)型はT型を参照するデータ型*11であると約束しておく。

　次のようにクラスTとインスタンスobjとobj2を作るコードを示す。

 T:{

     Ref(T) x = this;

}

Ref(T) obj = new T();

Ref(T) obj2 = new T();

obj2.x = new T();

obj.x = obj2.x;

obj.x.x = obj2;

　このxはダイクストラ選択で値を選出する方法よりも、while文など繰り返しの制御構造で値を選出するほうがより賢明である。

　例えば、

obj.x;

obj.x.x;

...

と一つずつ書くよりも、while文を使って、

Ref(T) ob = obj;

while (ob.x != obj2) {

  ob = ob.x;

  ...

}

と書いたほうがより賢くobjとobj2について探査ができる。

　ここでダイクストラ繰り返しについて考えてみよう。もし、このwhile文が計算停止不能と仮定すれば、ダイクストラのwhile文の定義より、繰り返しの有限性は以下のように明らかである。

if (ob.x !=  obj2) {

  ob = ob.x; //obはobj.x

  if (ob.x != obj2) {

    ob = ob.x; //obはobj.x.x

     if (ob.x != obj2) {  ...if(obj.x != obj2){...while(obj.x != obj2){...}} }

  }

}

ここで、obj.x != obj2、かつ、obj.x.x == obj2なのだから、すなわち、上のコードは、

if (TRUE) {

  ob = ob.x; //obはobj.x

  if (TRUE) {

    ob = ob.x; //obはobj.x.x

     if (FALSE) {  ...if(TRUE){...if(TRUE){...while(FALSE){...}}} }

  }

}

のように、FALSEを必ず含む無限のif文の入れ子となる。

　ゆえに、このwhile文の繰り返しは計算停止不能であれば有限であることが示せた。こうして、再帰データ構造の操作にはダイクストラ繰り返しの操作を用いることができる。

ダイクストラ不変量とクラスの抽象化

　以上により、公理化を除いたクラスについて抽象化をまとめてみよう。

  1. 第一段階（抽出）：Class、SubClass
  2. 第二段階（表現）：疑似コードClass:{...} SubClass<Class:{...}
  3. 第三段階（操作）：連接（SubClass<Class:{})、選択(obj.x = 12; obj.mehod())、繰り返し（Class:{Ref(Class) x;}、obj.x.x)

　抽象化の操作について、「連接」、「選択」は、常にダイクストラ不変量が成り立つのである。例えば、

PrefixClass:{

    int x = 0; //不変量 (x >= 0)

    int y = 0; // (x >= 0)

    procedure p() {

         x = x + 1; // (x >= 0)

    }

}

SubClass < PrefixClass:{

    int y = x-1; // (x >= 0)

    procedure q() {

         p(); // (x >= 0)

    }

}

Ref(PrefixClass) p = new PrefixClass();

p.x = 10; // (x >= 0)

p.m(); // (x >= 0)

Ref(SubClass) obj2 = new SubClass();

obj2.x = 12; // (x >= 0)

obj2.p(); // (x >= 0)

 

　このように、オブジェクトが生存しているかぎりは、必ず、ダイクストラ不変量 ( x >= 0) が成り立つことが保証される。また、その性質は再帰データ型で保全されている。そして、連接の注意点でも与えたように、我々がダイクストラ不変量を認識することはない。なぜならば、プログラムの途中で、

obj2.x = -1;

が入ること(バグ)を我々は予言できないからである。

　第４段階の公理化について興味のある人は、「構造化プログラミング」の第二部「データ構造化序論」を参照してほしい。

付録

　データ型の振る舞いをダイクストラ選択するには、疑似コードを使って次のようにすればよい。

Class: {

   int x = 12;

SubClass < Class : {

  string x = "h";

}

Ref(SubClass) obj = new SubClass();

Ref(Class) obj;

obj.x; // 文字列"h"

Ref(SubClass) obj;

obj.x; // 数値12

これはちょうど、古いPASCAL言語((「アルゴリズム+データ構造=プログラム」(ヴィルト著、片山卓也訳、科学技術出版社、昭和５４年９月１５日)))の可変レコードを使った直和の選択や、C++言語の名前空間の選択に似ている。

古いPASCAL言語の場合

type Union = 

   record

      case C (Class, SubClass) of

         Class: (x: int)

         SubClass: (x: char)

   end

end

 

Union obj;

 

case obj.C:

  Class: x := 12

  SubClass: x := "h"

 

C++言語の場合

obj.Class::x;  //12

obj.SubClass::x; //"h"

　直和のダイクストラ選択は、objのデータ型が変わっていないという点で、型キャストと異なる。

*1:『構造化プログラミング』ダイクストラ/ホーア/ダール　共著、　野下/川合/武市　共訳、サイエンス社、1975年8月）

*2:不変式とも訳される

*3:「Notes on Structured Programming」ダイクストラ、T.H.-Report- 70-WSK-03、1970年4月

*4:「系統的プログラミング」N.ヴィルト著、野下浩平、筧捷彦、武市正人共訳、近代科学社、2001年4月10日

*5:「Solution of a Problem in
Concurrent Programming Control」、E. W. DIJKSTRA、『Communications of the ACM』No.9 vol.5 、1965年9月

*6:ダイクストラはAlgol60をベースにしているが、この記事ではCに似たコードを採用した

*7:計算停止不能な計算における繰り返しの有限性の考察は後述する

*8:本文では手続きの拡張としている

*9:カルテジアン積、デカルト積ともいう。構造化プログラミングの原文では「cartesian product」だが、川合氏は「直積」と訳している

*10:手続き型という型とみなす

*11:データサイズの不明な動的構造で型の参照が必要