質問編集履歴

証明を追加

2018/12/21 09:17

投稿

退会済みユーザー

スコア0

test CHANGED Viewed

File without changes

test CHANGED Viewed

@@ -196,7 +196,7 @@
 記号 ⊢ を使用します。(ますます怪しくなるかもしれません。)
-前提列 ⊢ 結論　　前提列から結論を証明できることを意味する。(少なくとも一つ証明がある)
+前提列 ⊢ 結論　　前提列から結論を証明できることを意味する。(~~少なくとも一つ証明がある~~)
@@ -297,3 +297,105 @@
 {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|
+上記のいずれもトートロジーではない。*の行は前件が真で後件が偽となるため。
+分析タブロー、選言標準形、連言標準形も作成しましたが、全てトートロジーではありませんでした。
+この論証で良いと思いますが、問題があればご指摘ください。
+**解釈**
+「契約に基づく設計」は、サブクラスが事前条件、事後条件、不変条件を規則にしたがって弱めたり強めることでしか成り立たない。
+**結論**
+回答者、指摘者のお二人にお礼を申し上げます。ありがとうございました。ベストアンサーは復活させます。

質問の再提出

2018/12/21 09:17

投稿

退会済みユーザー

スコア0

test CHANGED Viewed

File without changes

test CHANGED Viewed

@@ -185,3 +185,115 @@
 **契約と状態管理**
 オブジェクトのライフサイクルで、内部状態の遷移を管理する必要があるか。直前像、直後像。ロールバックもサポートしなければならないか。
+### 質問やり直し - 勉強ました (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で描きたい
+Ps => Pw
+———————————-- 空文の規則
+{Ps} ; {Pw}      {Pw} S {Q}
+—————————————————————————————— 複合文（連接）の規則
+{Ps}  ;S  {Q}
+```
+**「弱める」の証明**
+```LaTexで描きたい
+                  Qs => Qw
+                ————————————— 空文の規則
+{P} S {Qs}       {Qs} ; {Qw}
+——————————————————————————————— 複合文（連接）の規則
+{P}  S;  {Qw}
+```

本論とは関係のない指摘に対するメモを残します

2018/12/14 10:12

投稿

退会済みユーザー

スコア0

test CHANGED Viewed

File without changes

test CHANGED Viewed

@@ -117,3 +117,71 @@
 「事前条件と事後条件の交差」の指摘については、合成関数のことだと推測しました。そうならばオーバーライドとは全く異なっていると思います。
+### 覚書 (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/09 03:19

投稿

退会済みユーザー

スコア0

test CHANGED Viewed

File without changes

test CHANGED Viewed

@@ -85,3 +85,35 @@
 ### 質問
 契約に基づく設計 (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は、スーパークラスの型を持つ変数に、サブクラスのインスタンスを代入して、ポリモーフィズム（多態性）を働かせるためには、（クライアントから見て）スーパー契約しかなく、サブ契約が変更できる余地は上に述べた通りだと言っています。その根拠がホーア論理です。契約と振る舞いは実質的に同じ意味です。
+「事前条件と事後条件の交差」の指摘については、合成関数のことだと推測しました。そうならばオーバーライドとは全く異なっていると思います。