Q&A
X, Y(ふるまい)は何を指しますか？
契約に基づく設計 (Design by Contract)
B. Mayerの契約に基づく設計では、ソフトウェアモジュールが提供するサービスをクライアントとサーバーの契約と捉え、以下を守ることになっています。
- 事前条件 サービス呼び出しの前にクライアントが守るべき義務
- 事後条件 サービスを提供する際にサーバーが守るべき義務
- 不変条件 守るべき、サービスの処理を通して一貫しているサービスの条件
スーパークラスを拡張してサブクラスを作成する場合、サブクラスの振舞いは上の条件を強めたり弱めることができる。サブクラスの振舞いです。
- 事前条件 弱めることができる
- 事後条件 強めることができる
- 不変条件 強めることができる
強める、弱めるの意味
含意 P => Q PからみてQは弱い。QからみてPは強いという。
命題P,Qを適用した集合を考えると、集合(P) ⊆ 集合(Q)
例えば、集合(P) = {x| x >=5 }、集合(Q) = {x| x > 0 }
包含関係でみるとおり、条件(命題)が偽になりやすいほど強いといい、真になりやすいほど弱いという。
ホーア論理 (Hoare Logic)
契約に基づく設計の根拠はホーア論理と書かれています。ホーア論理を調べると帰結規則というのが見つかりました。
事前条件を強める規則
Ps => Pw {Pw} S {Q}
———————————
{Ps} S {Q}
{Pw} S {Q} をサブクラスのメソッドと考えれば、PwがPsより弱められた事前条件になり、
帰結する {Ps} S {Q} はスーパークラスのメソッドと考えられます。
サブクラスからスーパークラスを証明することになり、契約に基づく設計とは議論が逆になると思います。
事後条件を弱める規則
{P} S {Qs} Qs => Qw
———————————
{P} S {Qw}
{P} S {Qs} をサブクラスのメソッドと考えれば、QsがQwより強められた事後条件になり、
帰結する {P} S {Qw} は、スーパークラスのメソッドと考えられます。
サブクラスからスーパークラスを証明することになり、契約に基づく設計とは議論が逆になると思います。
質問
契約に基づく設計 (Design by Contract) の議論とホーア論理 (Hoare Logic)の導出規則が逆になると思います。Xがスーパークラスの振る舞い、Yがサブクラスの振る舞いとすると。契約に基づく設計は、X => Y が成り立つといっているように思われますが、ホーア論理は、Y => X が成り立つといっています。両方成立するためには、X <=> Y でなければならないはず。これでいいのだろうか。根本的に間違っているかもしれないので、説明をお願いします。
訂正と補足 (2018-12-8)
訂正
B. Mayerと書きましたが、B. Meyerです。
補足
資料は次の通りです。
- 「オブジェクト指向入門 第２版 原則・コンセプト」バートランド・メイヤー著、酒匂寛訳 翔泳社 第１１章
- ‘Applying ‘Design by Contract”’ Bertrand Meyer IEEE Computer 1992 (画像版PDF) Introducing inheritance
質問に解説が抜けていたので補います。「契約が２つある」と指摘をいただきました。あとでスーパークラスの契約とサブクラスの契約だと気づきました。次に述べる理由からスーパークラスの契約しか存在しないと思っていたので指摘がわかりませんでした。
Meyerは、スーパークラスの型を持つ変数に、サブクラスのインスタンスを代入して、ポリモーフィズム（多態性）を働かせるためには、（クライアントから見て）スーパー契約しかなく、サブ契約が変更できる余地は上に述べた通りだと言っています。その根拠がホーア論理です。契約と振る舞いは実質的に同じ意味です。
「事前条件と事後条件の交差」の指摘については、合成関数のことだと推測しました。そうならばオーバーライドとは全く異なっていると思います。
覚書 (2018-12-9)
訂正と補足(2018-12-8)で書いた指摘の解釈が間違っているという指摘がありました。しかし私の質問の意図として上の説明は一貫性があるので、そのまま残します。
また、本題とは関係のない設計について詮索されたので、メモを残して忘れます。この覚書にコメントや回答はしないでください。
{P} S {Q} をどうするかは設計者に委ねられる。
- {True} S {P & Q} サービスが全責任を負う。Meyerは防衛的プログラミングとして退けている。
- {P & Q} S {True} サービスは何も供給しない。何をやっても良い。意味のある契約ではない。
- {Q} S {P} これは{P} S {Q} とは別の契約だが実例はあるか。(上の質問の証明とは本質的に異なる。)
(ここが２つの契約や交差についての解釈が間違っているという指摘に該当すると思われる)
Pの中でクライアントが知り得ないオブジェクトのカプセル化された情報を使ってはならない。
{Pa & Pb & … Pn} S {Q}は以下のように変形できる。
{Pb & … Pn} S {Q & Pa} Pを事後条件に移動すると防衛的プログラミングに近づくだろう。
不変条件
I を不変条件とすると、{P} S {Q} は次のとおり。
{I & P} S {I & Q} Meyerは全てのメソッドに不変条件を書かなければならないのなら、言語が１箇所でサポートすべきと言っている。
(C#はアドオンとして契約設計を提供。言語自体が不変条件をサポートするわけではないので、どう扱うのだろう)
(C#のドキュメントには限量子∀、∃が登場していたので述語論理が基礎にある。理論的根拠に興味がある。)
ADT
一つのメソッドの振る舞い(契約)を考察したが、オブジェクトの仕様としてADT(Abstract Data Type)を導入している。ADTとして公理を検討すれば、各メソッドで何をP、Qにするかは決めやすい。ADTから設計を開始すべきだろう。
ADT資料
- 「オブジェクト指向入門 第２版 原則・コンセプト」
- 「独習コンピュータ科学基礎II」米国で評判が悪い。
- リスコフがMITで始めた授業（の別人による改訂版）がオンラインで受けられる。コースの評判は良い。
契約と状態管理
オブジェクトのライフサイクルで、内部状態の遷移を管理する必要があるか。直前像、直後像。ロールバックもサポートしなければならないか。
質問やり直し - 勉強ました (2018-12-14)
証明を少し勉強しました。この質問は証明の構成を問題にしたつもりですが、証明をうまく説明できないので、曖昧でした。質問を再提出します。初心者なので説明が怪しいかもしれません。
記号 ⊢ を使用します。(ますます怪しくなるかもしれません。)
前提列 ⊢ 結論 前提列から結論を証明できることを意味する。(少なくとも一つ証明がある)
ホーア論理
ホーア論理の証明の構成は以下のとおり。サブクラスからスーパークラスを証明する。
Ps => Pw, {Pw} S {Q} ⊢ {Ps} S {Q} <— 事前条件を強める
{P} S {Qs}, Qs => Qw ⊢ {P} S {Qw} <— 事後条件を弱める
契約設計の主張と証明の向き
契約設計の主張のとおりに、スーパークラスからサブクラスを証明することはできないか。
Ps => Pw, {Ps} S {Q} ⊢ {Pw} S {Q} <— 事前条件を弱める (1)
Qs => Qw, {P} S {Qw} ⊢ {P} S {Qs} <— 事後条件を強める (2)
この証明を立てることに意味があるのだろうか？今の自分の実力では、証明も反証もできません。
以下は証明できそうだと思いますが、上の証明とは異なります。
(1)の前提列 ⊢ {Ps} S {Q ∧ Pw}
(2)の前提列 ⊢ {P ∧ Qs} S {Qw}
解釈
初心者の素朴な質問として。スーパークラスからサブクラスへ向かう証明が可能/不可能とした場合、契約設計の意味は？スーパークラス単独で、契約を保証するために、サブクラスを統治する規則は作れないのか？言い換えると、サブクラスの自発性に委ねるしかないのが、契約設計なのか？
質問
- ホーア論理はサブクラスからスーパークラスの動作（契約）を証明している。証明は契約設計の理論的な根拠になりうるのか？
- 契約設計の言うとおりに、スーパークラスからサブクラスへ向かう証明を考えることは意味があるか？しかし自分で証明/反証できません。
- 解釈：証明をもとに契約設計の解釈(意味の考察)をしたい。
最後の素朴な質問が、ホーア論理を学んだとき、これを考えた動機です。質問はハウツーで答えられるものではなく、曖昧です。この場(teratail)にふさわしくなければ取り下げます。ベストアンサーは一時的に外します。ごめんなさい。
以上です。怪しいところは遠慮なく回答でご指摘ください。
追加：やってみたこと。自分の勉強です。
ホーア論理を自分で証明してみました。推論は正しいか？
「強める」の証明
LaTexで描きたい
1Ps => Pw 2———————————-- 空文の規則 3{Ps} ; {Pw} {Pw} S {Q} 4—————————————————————————————— 複合文（連接）の規則 5{Ps} ;S {Q}
「弱める」の証明
LaTexで描きたい
1 Qs => Qw 2 ————————————— 空文の規則 3{P} S {Qs} {Qs} ; {Qw} 4——————————————————————————————— 複合文（連接）の規則 5{P} S; {Qw}
証明 (2018-12-21)
契約設計の主張と証明の向き
契約設計の主張のとおりにスーパークラスからサブクラスを証明する。
Ps => Pw, {Ps} S {Q} ⊢ {Pw} S {Q} <— 事前条件を弱める (1)
Qs => Qw, {P} S {Qw} ⊢ {P} S {Qs} <— 事後条件を強める (2)
証明方法
(1),(2)を証明するには以下の(a),(b)がトートロジー(恒真)であることを示せば良い。トートロジーでなければ証明は不成立。
(Ps => Pw ∧ {Ps} S {Q}) => {Pw} S {Q} <— (a) (1)の推論
(Qs => Qw ∧ {P} S {Qw}) => {P} S {Qs} <— (b) (2)の推論
そのために、真理値表、分析タブロー、選言標準形、連言標準形のいずれかを作成する。
(清水義夫 『記号論理学』 東京大学出版会 1984年)
(a)の真理値表
| Ps | Pw | Q | Ps => Pw | {Ps} S {Q} | {Pw} S {Q} | (Ps => Pw ∧ {Ps} S {Q}) => {Pw} S {Q} |
|---|---|---|---|---|---|---|
| F | F | F | T | T | T | T |
| F | F | T | T | T | T | T |
| F | T | F | T | T | F | F* |
| F | T | T | T | T | T | T |
| T | F | F | F | F | T | T |
| T | F | T | F | T | T | T |
| T | T | F | T | F | F | T |
| T | T | T | T | T | T | T |
(b)の真理値表
| P | Qs | Qw | Qs => Qw | {P} S {Qw} | {P} S {Qs} | (Qs => Qw ∧ {P} S {Qw}) => {P} S {Qs} |
|---|---|---|---|---|---|---|
| F | F | F | T | T | T | T |
| F | F | T | T | T | T | T |
| F | T | F | F | T | T | T |
| F | T | T | T | T | T | T |
| T | F | F | T | F | F | T |
| T | F | T | T | T | F | F* |
| T | T | F | F | F | T | T |
| T | T | T | T | T | T | T |
上記のいずれもトートロジーではない。*の行は前件が真で後件が偽となるため。
分析タブロー、選言標準形、連言標準形も作成しましたが、全てトートロジーではありませんでした。
この論証で良いと思いますが、問題があればご指摘ください。
解釈
「契約に基づく設計」は、サブクラスが事前条件、事後条件、不変条件を規則にしたがって弱めたり強めることでしか成り立たない。
結論
回答者、指摘者のお二人にお礼を申し上げます。ありがとうございました。ベストアンサーは復活させます。
厳密ではないかもしれませんが{P}S{Q}だと思っています。{事前条件}処理{事後条件}のセット。
そうなると、X => Y はどういう意味になりますか？
スーパークラスの{事前条件}処理{事後条件}からサブクラスの{事前条件}処理{事後条件}を導出すること。逆にサブクラスからスーパークラスとも。そう思っています。よろしくお願いします。
強い弱いと同じ記号ですが、違う意味ということですね？
それと「導出」の定義もしてください。何を持って導出としますか？
初心者なので証明できるとしかいえません。証明に使う規則はホーア論理の規則と論理規則になると思います。これは質問に含めたいのですが、自分でも考えるべきだと思います。
強い弱いと同じ記号ですが、違う意味ということですね？ <-- どの記号ですか。
Ps => Pw と X => Y は違う意味なのですね？
=> これは含意です。P => Q は、 not P or Q に等しいです。
つまり同じ記号を二種類の意味で使っているということではありませんか？
=> は、論理学では「前件」が成立すれば「後件」も成立するという意味です。「前件」=>「後件」。インターネットで調べた例を書きます。「xは砂糖である」ならば「xは甘い」。砂糖の集合は甘いものの集合に含まれるので、強い弱い（英語圏の言い方のようです）の関係は「xは砂糖である」>「xは甘い」になるそうです。強いほうが条件がきつくなると考えてください。
⇒ で書き直した方が通じるのでは？
ごめんなさい。そうすべきでした。
あと X ⇒ Y は明らかに誤りです。
なぜですか。それを知りたい。回答してください。
質問の意味をまだはかりかねているので回答できません。ふるまいだとすればそれは条件ではないので成り立ちません。
継承した場合、まったく別のふるまいでオーバーライドされます。
継承しても契約は守らなければなりません。契約とは、自動販売機にたとえれば、100円くれたら（事前条件）、かならず缶ジュースを提供する（事後条件）ことです。継承して内部処理が変わったとしても契約は守らなければならない。そこでできることは、事前条件は弱めることだけができて、事後条件は強めることだけができる。その理論的根拠がホーア論理ですが、ホーア論理は逆を証明しているのでわからなくなりました。
契約ではなくふるまいなのでしょう？
契約だとすると、二つの契約が X に含まれます。X と Y 合わせて四つです。包含関係も交差しますので成り立ちません。
つまり、X ⇒ Y が成り立つという前提がそもそも間違っています。
多分、論理学ではなくコーディングを学んだ方がいいと思います。C# だと Contract が簡単に使えますから、それを見てイメージしてみてはどうでしょう？
わからなくなりました。二つの契約とはなんですか。包含関係が交差することもわかりません。
X ⇒ Y が成り立たつ必要がなく Y ⇒ X だけで「契約に基づく設計」が「ホーア論理」で説明できるのなら、それを解説してください。
Y ⇒ X も成り立ちません。
事前条件と事後条件の二つ、正確には不変条件を入れて三つですが、事前条件と事後条件の二つは継承によって強弱関係が交差します。片方は強くなり、片方は弱くなります。
その根拠を教えてください。勉強します。
今書いたところですが、わかりにくいところはどこでしたか？
そもそも契約に基づく設計をしたことがありますか？
どこがわかりにくかったですか？ --> 契約が二つになること。事前条件を満たすか満たさないか。事後条件をみたすか満たさないかでシナリオが異なると言っていますか。強弱関係が、片方が強くなり、片方が弱くなるのは、継承すると必ずそうなるのでしょうか。それとも強弱どちらにも変化できて組み合わせを考えなければならないということですか。
シナリオというのが何を意味するかわかりませんが、なぜ成り立つと思うのですか？
継承するとそうなるのではなく、そのように設計するのが契約による設計です。
そもそも契約に基づく設計をしたことがありますか？ --> ありますが、サブクラスを含めておっしゃっている意味ではできていないのでしょうね。
でなければ多態性が崩壊します。
サブクラスを含めなければこの質問が破綻します。
方向がずれてきているようなので、わからないところは宿題とさせてください。時間がかかっても私は理解したいだけです。C#の資料を少しみました。今日ダウンロードしたリスコフの論文に出ていた内容が含まれているようです。時間がかかるかもしれませんが頑張ってみます。
お礼を忘れていました。長い時間ありがとうございました。情報も。
いいえ。お役に立てませんでした。
勘違いしていたかもしれません。関数 f によって事前環境(変数の値など)が事後環境にどう変化するかという約束を契約と思っていませんか？ 契約に基づく設計で言うところの契約はそのような振る舞いのことではありません。プログラミングで「条件」というのは true または false のことで、f を実行するにあたり事前に true でなければならない式を事前条件、事後に true とならなければならない式を事後条件と言い、事前条件、事後条件、不変条件の全てに true を保証するという契約を満たすようにプログラミングするのが契約に基づく設計です。
具体的に言うと、例えば f(x) = x + 1 という式を実行するにあたり、「ただし x は自然数」という条件が事前についていれば、それは「x は自然数」という条件が事前に真となることが求められています。この事前条件を満たすという契約がユーザーと制作者の間で交わされています。そこで f を実行する前に契約が履行されているかどうかを確認し、f の実行時にそれを保証するように作るのが契約に基づく設計となります。
またホーア論理というのはプログラムの正当性を推論するためのものですから swordone さんのおっしゃる通り、契約に基づく設計が正当であることを証明するために使われたと見るのが妥当かと思います。
ありがとうございます。感謝します。
追記読みましたが通じてないみたいですね。契約に基づく設計をしたことがあるとのことですが、したことないと思いますよ。根本的な勘違いがあります。
ありがとうございます。参考資料C#を読んで考えてみます。もしよろしければ回答を使ってご教授ください。
追記を読んで呆れました。聞く耳持たないようですが、質問ではなくドヤりたいだけなら Qiita かブログへどうぞ。これ以上のコメントも追記も不要です。続きはそちらへ。
念のため付け加えておきますが、私があれこれ聞いたのはあなたの使う用語が怪しかったから、いや今現在もって怪しいからです。
ドヤるの意味がやっとわかりました。質問をさいていしゅつしました。
回答1件
0
ベストアンサー
そもそもホーア論理は「契約に基づく設計」において、「事前条件を強めることができる」ことや「事後条件を弱めることができる」事の証明をしているのではないですか？
「サブクラスからスーパークラスを証明する」の意味が分かりませんが、そこで証明しているのは
- サブクラスで事前条件を弱めたものはスーパークラスの事前条件を満たす
- サブクラスで事後条件を強めたものはスーパークラスの事後条件を満たす
事だと思われますので、この議論で全く問題ないように思われます。
投稿2018/12/05 22:02
総合スコア20651
ありがとうございます。証明を勉強します。
あなたの回答
tips
プレビュー
