[debian-users:12139] Re: historical info

[Mitsuru Oka <oka@debian.or.jp>]

岡＠情報科学.高知大です。# 時間が無いくせに沢山書いてる^^;


"樽石"すなわちMasato Taruishiさんより:

> 樽石さんがどういう意味で事前条件とおっしゃってるのかよく分か
> らないですが、僕の言ってるのは Hoare の公理意味論における
> pre-post formula です(こっちの言語理論って学部でやるのかな??)。

樽石> うーむ、わかりません。どういう理論でしょう？

話は多岐に渡りますが、基本だけ書くと、事前条件 P、事後条件 Q
として、

 {P} a {Q}

と書くとき、「P が満たされている時に a を実行されて、かつそ
の実行が終了したときには、Q を満足する」を意味します。

ちょっと引用すると、

 {y > 0} x := y {x > 0}

です。直感的には、あたりまえの事を説明しているだけです。関数
(もちろん純粋な関数です)の引数に与える制約条件が事前条件、得
られる返り値に与える制約条件が事後条件だと思えば、だいたい分
かると思います。
これと導出規則等を使えば、プログラムの正しさを証明する
ことさえある程度可能です(当然無限ループとかがネックになる)。

参考書は、共立出版のオレンジの本にもあった筈ですが、僕は個人
的に B.Meyer が気に入ってるので ASCII の「プログラミング言語
理論への招待」を使ってます。かなりオブジェクト指向な切り口で
読める筈です。# もちろん、「オブジェクト指向入門」も。

# すごい話が逸れてる...。


> dpkg-divert はあくまで「作用」をもたらすものでしょう?

樽石> それは、問題なのでしょうか？
樽石> 他に対して「作用」を要求するのはごく一般的だとおもいますけど。。。

確かに一般的に見うけられます、それに馴染んでしまうと僕の書い
てる事はちょっと遠回りに見えます(実際遠回りですが)。例えば、
手続き型と宣言型を思い浮べてみたらちょっと分かるかも。今の
postinst あたりは手続き型の典型ですが、じゃなくて、もっと抽
象化した要求ないしは条件を記述するに留めるんです。パッケージ
の性質を宣言する。

# 当然、{pre,post}{inst,rm} なんてカテゴリは不必要になります。
# いつ何を実行するかは、システムが考えることですから。


樽石> 具体的にどう問題でどうするのが良いのか教えてください。
樽石> #僕が、現状思っている問題は、システム状態の変更が、実行時まで
樽石> #判明しないというのがあります(alternatives なんかは最初にわかって
樽石> #いると便利)。

これはあっちこっちに書いちゃいましたね。

> カプセル化の実体こそ、ルール記述(=データ)と制御(=手続き)の明
> 確な分離です。オブジェクト=データ+手続きと言うと、よく、両者
> をごちゃまぜにすることと混同される方がいるようですが、混ぜる
> のではなくて明確に切り分けて考える行為です。

樽石> 岡さんがいうルールと制御の分離はカプセル化を念頭においてる
樽石> ものなのでしょうか？僕は、ルールはルールとして、dpkg に処理
樽石> させて、そのあと制御を実行するという分離を言っているんだと
樽石> 思っているのですが。

樽石さんが書いていたのにちょっと反論して書いただけで、カプセ
ル化を意識しているわけではないです。それよりむしろ、いかにデー
タフォーマットたり得るか、を考えています。例えて言えば、
PostScript と PDF、DynamicHTML と XML(as Web Data) って所
でしょうか、対極的でしょう? # 言葉少なすぎるかな...。


> 実行ファイルであることが問題なんです。

樽石> これは、予想外の行動もできるという意味で問題なんでしょうか？
樽石> それとも、パッケージ側には全く実行を許さないということでしょうか？

そんな所です。あと、うまく説明できない何かがあるんですが...。
例えば、パッケージにバグがあるとよく、次のバージョンの
postinst あたりで対処したりしますが、あれが癌なんです。もっ
と問題を直視できる方法はないものか、と。


樽石> 僕は現状の dpkg のシステムを (簡易)Java であらわすなら以下のような
樽石> 位置づけでないかと思っています。

樽石> interface Package {
樽石>   preinst(Object obj);
樽石>   postinst(Object obj);
樽石>   ...

樽石> class Dpkg {
樽石>  .... 

樽石>  /** Package をインストールする。 中身の記述は適当 */
樽石>  public void install(Package pkg) throws DpkgException {
樽石>    pkg.preinst(new DpkgAction("install"));

これなかなか面白いですね。

--
岡 充 (Mitsuru Oka)
高知大学理学部情報科学科4回生