2005/09/28 志村先生 アルゴリズムの正当性証明と論理 人間のかいたプログラムには、かいた人間の意図がある プログラムのすることが、かいた人間の意図にそっているかどうかが問題 cf. プログラムのバグ 思いもよらない所で、思いもよらない結果が... => これをさけるにはどうすればよいか ? 一番確実に、このような問題をさける方法は .. ? プログラムの動作が望んだ通りの結果になることを「数学的」に証明すること # その方法にも、色々な形がある [証明の対象] アルゴリズム、プログラム、システム 「ある条件が成立していると、ある動作を行う」ことをチェックする cf. 交差点システム 交通事故という状態はおきないということを示したい。 cf. 共有システム 「かりたら返す」は、きちんと動くか ? 「だれがかりたか」が解る仕組が必要 [証明の対象の定式化] 多数のプロセスが関係する 永続的に動作する応答システム ( 外からの入力に対して出力を行う ) プログラムの分類 単純なシステム cf. 数値計算プログラム 目的が明確、値が得られると停止する # 他の存在を想定しない 協調システム cf. OS ( 単一プロセッサー内の複数プロセス ) 他のプロセスを仮定しているプログラム cf. 並列計算 ( 複数プロセッサー上の複数プロセス ) 他のプロセッサーの存在を仮定しているプログラム 複数のプロセスにおける問題点 => 資源の共有 cf. メモり共有 ( 複数のプロセスが同一のメモり空間を共有している ) 特定な番地のメモりの内容を複数のプロセスが扱うとどうなるか ? 一つのプロセスのメモり書換えを他のそのメモりを利用するプロセスが知らなかったら... ? 変なことがおきても不思議はない # 計算機の世界でなくても色々と在りうる cf. ATM の例 ( 銀行で、預金の引き出しを行う場合を考える ) [引き出しプロセス(動作)] [ATM 側] 1. 口座番号, 引出し額, etc.. ATM -> CC 2. 引き出し Ok ならば、その額の現金を出す ATM -> 人間 3. 支払額の報告 ATM -> CC [Center Computer 側] ( 預金を管理 ) 1. 口座番号, 引き出し額, etc.. 見て、引き出し可能かどうかを判定 CC <- ATM 2. 引き出し可能ならば、要求のあった ATM に OK を送る CC -> ATM 3. 預金残高から引き出し額を減じる [単一プロセスの場合の流れ] A.1 -> C.1 -> C.2 -> A.2 -> A.3 -> C.3 これは、望み通りだが... [複数プロセスの場合は .. ?] CC は一台だが、ATM は複数台ある.. ATM が二台あった場合のシナリオ 50000 の預金があるとする ATM 1 預金管理 ATM 2 | | | | 30000 要求 | 50000 | +-------------> | | | | | | OK | | | <-------------+ | | | | | | 40000 要求 | | | <---------------------+ | | | | | OK | | +---------------------> | | | | | 引き出し結果 | | +-------------> | 20000 | | | 引き出し結果 | | | <---------------------+ | | | | | -20000 ??? | | | | 何が問題か ? 二つのプロセス (ATM1,ATM2) が共有している資源 (預金高) を両方が「同時に利用している」こと => 共有資源は、一方が触っている間他方は触れない仕組が欲しい 明らかな対策は、「プロセスを一つにする」ことだが.. => これは認められない !! # 対策によって、他のプロセスが扱えない状況がおきるのも許されない # => 共有資源は「いつかは利用できる」という保証も必要 共有資源が複数の場合の問題 二人の人間が、食事をするのに一本ずつのナイフとフォークの両方を必要としているとする 一方が、ナイフを他方が、フォークを一本ずつつ取るとどうなるか... ? => 両方が餓死に... (デッドロック) == 複数のプロセスが関る問題をどのように記述するか ? # その方法も色々あるが... => 形式論理を用いて記述する 「仕様」 : プログラムの機能 ( 本来、どのように動いて欲しいか.. ? ) を記述したもの 仕様を論理式で表す 正当性の証明 仕様を表す論理式を形式的に証明する # 単一のプロセスのアルゴリズムでも同様なアプローチは可能 # => 複数のプロセスや応答を含むプロセスを論理式で表現するのは難しい # => 「時間」を表す仕組が必要 形式的論理としては、時間の概念を表すことができなければならない。 「時間」の概念にも様々あるが... 2005/09/28 11:31:53 までを表現する必要はあるか ? => 定量的なものまでを扱うと大変 とりあえず、「定量的な問題」は考えない (方針) # かなり「いい加減」な立場 時刻の前後関係だけを表すようにする 因果関係 : 原因が過去にあって、結果が未来にある => Temporal logic ( 時間論理 ) # 前期にちょっとふれた == Temporal logic # 流儀が色々あるが、ここでは... # => F, G という様相を用いる流儀で行う G p : これから先ずっと、 p が成立する F p : これから先いつか、 p が成立することがある == [「時間」を扱う上での問題点] 時間の構造 連続的 v.s. 離散的 # 古典的, 物理的には、「連続」にきまっている # しかし、扱いたい問題は、「離散」で十分 # 現実を全て論理でシミュレートするつもりはない # 計算機では、クロック(離散時刻)がある # 問題を「離散的」に考えた方が「簡単」 線型 v.s. 分岐 # 現実の世界は、「線型(一つの流れ)」しかない # 時間が分岐するモデルもある # => 並列計算 # 組み合わせは 2 x 2 の 4 通りだが、通常は、「連続=分岐」は扱わない == [離散=線型] ↓ ... --O----O----O----O----O----O----O----O-- ... Gp p p p p p p ↓ ... --O----O----O----O----O----O----O----O-- ... Fp p p # 追加の様相 # 離散の場合は「次の時間」があるので、これを扱う様相があると便利 X p : 次の時刻で p が成立 ↓ ... --O----O----O----O----O----O----O----O-- ... Xp p p p U q : p が成立するまで p が成立している ↓ ... --O----O----O----O----O----O----O----O-- ... pUq p p p q # 強い U と弱い U がある # 強い U : いつかは必ず q が成立する (停止する) # 弱い U : q が成立することがないかも.. ( その場合は、ずっと、p が成立する ) # この程度の表現能力があると、「問題を記述する側」は便利 # 裏返せば、それだけの表現能力を実現するの ( 公理系 ) が大変 [定理] F は G で表すことができる F p ≡ ¬G ¬p [定理] G は U で表すことができる G p ≡ p U (q ∧¬q) [これらの記号を用いて表現可能な有用な概念] F G p : ある時点から先ずっと p が成立する。 F^∞ p = G F p : この先、 p が成立することが無限に起きる。 F p では現時点での有限先で、p が成立すること意味する # これは時間のモデルを「離散」に選んだから.. しががって、 次に p が成立する時点でも F p が成立するので、無限に p が成立することになる。 # 時間のモデルを決定すると、自動的に成立する命題がしょうじることになる、上記はそのような例の一つ p B q = ¬((¬p)Uq) : q が起きるならば、その前に p が成立する == 次回以降は、「問題をどのように時間論理で表現するか ? 」について説明する。