質問をすることでしか得られない、回答やアドバイスがある。

15分調べてもわからないことは、質問しよう!

ただいまの
回答率

88.61%

契約に基づく設計 (Design by Contract) とホーア論理 (Hoare Logic) の関係がわかりません。

解決済

回答 1

投稿 編集

  • 評価
  • クリップ 0
  • VIEW 1,032
退会済みユーザー

退会済みユーザー

契約に基づく設計 (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です。

補足
資料は次の通りです。

  • 「オブジェクト指向入門 第2版 原則・コンセプト」バートランド・メイヤー著、酒匂寛訳 翔泳社 第11章
  •  ‘Applying ‘Design by Contract”’ Bertrand Meyer IEEE Computer 1992 (画像版PDF) Introducing inheritance

質問に解説が抜けていたので補います。「契約が2つある」と指摘をいただきました。あとでスーパークラスの契約とサブクラスの契約だと気づきました。次に述べる理由からスーパークラスの契約しか存在しないと思っていたので指摘がわかりませんでした。

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} とは別の契約だが実例はあるか。(上の質問の証明とは本質的に異なる。)
    (ここが2つの契約や交差についての解釈が間違っているという指摘に該当すると思われる)

Pの中でクライアントが知り得ないオブジェクトのカプセル化された情報を使ってはならない。

{Pa & Pb & … Pn} S {Q}は以下のように変形できる。
{Pb & … Pn} S {Q & Pa} Pを事後条件に移動すると防衛的プログラミングに近づくだろう。

不変条件
I を不変条件とすると、{P} S {Q} は次のとおり。
{I & P} S {I & Q}  Meyerは全てのメソッドに不変条件を書かなければならないのなら、言語が1箇所でサポートすべきと言っている。
(C#はアドオンとして契約設計を提供。言語自体が不変条件をサポートするわけではないので、どう扱うのだろう)
(C#のドキュメントには限量子∀、∃が登場していたので述語論理が基礎にある。理論的根拠に興味がある。)

ADT
一つのメソッドの振る舞い(契約)を考察したが、オブジェクトの仕様としてADT(Abstract Data Type)を導入している。ADTとして公理を検討すれば、各メソッドで何をP、Qにするかは決めやすい。ADTから設計を開始すべきだろう。

ADT資料

  • 「オブジェクト指向入門 第2版 原則・コンセプト」
  • 「独習コンピュータ科学基礎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)にふさわしくなければ取り下げます。ベストアンサーは一時的に外します。ごめんなさい。

以上です。怪しいところは遠慮なく回答でご指摘ください。

追加:やってみたこと。自分の勉強です。

ホーア論理を自分で証明してみました。推論は正しいか?

「強める」の証明

Ps => Pw
———————————-- 空文の規則
{Ps} ; {Pw}      {Pw} S {Q} 
—————————————————————————————— 複合文(連接)の規則
{Ps}  ;S  {Q}

「弱める」の証明

                  Qs => Qw
                ————————————— 空文の規則
{P} S {Qs}       {Qs} ; {Qw}
——————————————————————————————— 複合文(連接)の規則
{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

上記のいずれもトートロジーではない。*の行は前件が真で後件が偽となるため。
分析タブロー、選言標準形、連言標準形も作成しましたが、全てトートロジーではありませんでした。
この論証で良いと思いますが、問題があればご指摘ください。

解釈
「契約に基づく設計」は、サブクラスが事前条件、事後条件、不変条件を規則にしたがって弱めたり強めることでしか成り立たない。

結論
回答者、指摘者のお二人にお礼を申し上げます。ありがとうございました。ベストアンサーは復活させます。

  • 気になる質問をクリップする

    クリップした質問は、後からいつでもマイページで確認できます。

    またクリップした質問に回答があった際、通知やメールを受け取ることができます。

    クリップを取り消します

  • 良い質問の評価を上げる

    以下のような質問は評価を上げましょう

    • 質問内容が明確
    • 自分も答えを知りたい
    • 質問者以外のユーザにも役立つ

    評価が高い質問は、TOPページの「注目」タブのフィードに表示されやすくなります。

    質問の評価を上げたことを取り消します

  • 評価を下げられる数の上限に達しました

    評価を下げることができません

    • 1日5回まで評価を下げられます
    • 1日に1ユーザに対して2回まで評価を下げられます

    質問の評価を下げる

    teratailでは下記のような質問を「具体的に困っていることがない質問」、「サイトポリシーに違反する質問」と定義し、推奨していません。

    • プログラミングに関係のない質問
    • やってほしいことだけを記載した丸投げの質問
    • 問題・課題が含まれていない質問
    • 意図的に内容が抹消された質問
    • 過去に投稿した質問と同じ内容の質問
    • 広告と受け取られるような投稿

    評価が下がると、TOPページの「アクティブ」「注目」タブのフィードに表示されにくくなります。

    質問の評価を下げたことを取り消します

    この機能は開放されていません

    評価を下げる条件を満たしてません

    評価を下げる理由を選択してください

    詳細な説明はこちら

    上記に当てはまらず、質問内容が明確になっていない質問には「情報の追加・修正依頼」機能からコメントをしてください。

    質問の評価を下げる機能の利用条件

    この機能を利用するためには、以下の事項を行う必要があります。

質問への追記・修正、ベストアンサー選択の依頼

  • 退会済みユーザー

    退会済みユーザー

    2018/12/08 12:45

    ありがとうございます。参考資料C#を読んで考えてみます。もしよろしければ回答を使ってご教授ください。

    キャンセル

  • Zuishin

    2018/12/09 12:27 編集

    追記を読んで呆れました。聞く耳持たないようですが、質問ではなくドヤりたいだけなら Qiita かブログへどうぞ。これ以上のコメントも追記も不要です。続きはそちらへ。

    念のため付け加えておきますが、私があれこれ聞いたのはあなたの使う用語が怪しかったから、いや今現在もって怪しいからです。

    キャンセル

  • 退会済みユーザー

    退会済みユーザー

    2018/12/14 20:23

    ドヤるの意味がやっとわかりました。質問をさいていしゅつしました。

    キャンセル

回答 1

checkベストアンサー

+2

そもそもホーア論理は「契約に基づく設計」において、「事前条件を強めることができる」ことや「事後条件を弱めることができる」事の証明をしているのではないですか?
「サブクラスからスーパークラスを証明する」の意味が分かりませんが、そこで証明しているのは

  • サブクラスで事前条件を弱めたものはスーパークラスの事前条件を満たす
  • サブクラスで事後条件を強めたものはスーパークラスの事後条件を満たす

事だと思われますので、この議論で全く問題ないように思われます。

投稿

  • 回答の評価を上げる

    以下のような回答は評価を上げましょう

    • 正しい回答
    • わかりやすい回答
    • ためになる回答

    評価が高い回答ほどページの上位に表示されます。

  • 回答の評価を下げる

    下記のような回答は推奨されていません。

    • 間違っている回答
    • 質問の回答になっていない投稿
    • スパムや攻撃的な表現を用いた投稿

    評価を下げる際はその理由を明確に伝え、適切な回答に修正してもらいましょう。

  • 2018/12/08 09:47

    ありがとうございます。証明を勉強します。

    キャンセル

15分調べてもわからないことは、teratailで質問しよう!

  • ただいまの回答率 88.61%
  • 質問をまとめることで、思考を整理して素早く解決
  • テンプレート機能で、簡単に質問をまとめられる

関連した質問

同じタグがついた質問を見る