2008-09-10 [長年日記]
λ. 帰りに泳いできた
帰りに近くのプールで泳いできた。例によって1kmを30分くらいで。 泳いでいたら、すごく肩がこっていたことに気づく。 それがほぐれて(?)気持ちいい。 いい運動したし、今日はよく眠れそうだ。
λ. ソフトウェア仕様の差分について by 石井忠夫
ソフトウェアの発展問題というのを型理論で扱おうという話。 ソフトウェア発展問題というのは以下のような問題。
今、考えている発展問題に現れうる全ての仕様の集合をS、全てのプログラムの集合をPとし、ある仕様 S∈S からプログラム P∈P が導かれることを S⊢P と表す。 また、仕様とプログラムの集合にある順序関係 ⊑ を導入し、仕様 S が S' に発展することを S⊑S' と表す。 この時、ソフトウェア発展問題は仮定 S⊢P 及び S⊑S' の下で、条件 P⊑P' 及び S'⊢P' を満すプログラム P' を見出すことと定式化される。 ここで、仕様の発展 S⊑S' が任意であれば、両者に共通部分が無くプログラム P' は新規に実現する必要がある。 他方、両者に共通部分が多く含まれ、両仕様の差分を活用して P から P' が効果的に実現される時には発展問題を考えることができる。
でもって、型理論での型=仕様, 項=プログラムという枠組みで、型と項にそれぞれ順序 ⊑ と、合併⊕、差分⊖、共通部分⊗を定義して、このソフトウェア発展問題を形式化しようとしている。 ただ、導入した順序がソフトウェアの発展をどの程度表現できているのかはちょっと疑問。
[ツッコミを入れる]
