ノート:契約プログラミング

事前条件・事後条件 と obligation・benefit

(@Poshnegev:) Eiffel のサイトのこれ [1] ですが、 表が書き間違っているだけでしょう。表の下の文章をちゃんと読んでください。

* Note how the obligation for each of the parties maps onto a benefit for the other.

* The client's obligation, which protects the supplier, is called a precondition.

さらに §Preconditions でも bottom-right と書いている。

* The client's benefit, which describes what the supplier must do (assuming ～), is called a postcondition.

これは 表の下段 ("Supplier"の行) に書かれている "precondition" ＆ "postcondition" とは合わない（逆になっている）。 文章の方が論理的に筋が通っているので、表の方が書き間違いだろう、となります。

他の資料を見ると、 講義資料のようですが 例えばこれ↓だと正しく書かれています。

Object-Oriented Software Construction (Bertrand Meyer) Lecture 9: Design by Contract

--RnTkm（会話） 2021年11月11日 (木) 10:09 (UTC)

返答です

• Note how the obligation for each of the parties maps onto a benefit for the other.
  （それぞれの当方の義務表記は、先方の利益表記にマッピングされる）

↑これは顧客の義務（左上の料金を払う）は、業者の利益（右下の料金不正なら未実行）にクロスマッピングされ、業者の義務（左下の電話サービス提供）は、顧客の利益（右上の電話サービス利用）にクロスマッピングされるという意味です。辻褄はあってる思います。

• The client's obligation, which protects the supplier, is called a precondition.
  （業者を（不正パラメータから）保護する顧客の義務は、事前条件と呼ばれる）

↑辻褄はあってる思います。

• The client's benefit, which describes what the supplier must do (assuming the precondition was satisfied), is called a postcondition.
  （業者がなすべきこと（事前条件のことを満たすように）を記述している顧客の利益は、事後条件と呼ばれる）

↑辻褄はあってると思います。

• An apparent paradox of Design by Contract™, which is reflected in the bottom-right entries of the preceding and following contract tables,
  （契約による設計の明白なパラドックスは、契約テーブルの遂行前後での図表右下のエントリにおいて反映されている）

↑これは、図表右下の業者の利益（サービスしない）が、図表左上の顧客の義務（正しい支払い）を顧客自身がチェックして決定するという現実社会から見たらおかしな仕組みを（客が自分で支払い審査するなどあり得ない）パラドックスとしている文章です。Eiffleのメソッド本体には自動パラメータチェック機能がないのでコール側で事前パラメータチェックをすることに由来しています。辻褄はあってる思います。

--Poshnegev（会話） 2021年11月11日 (木) 12:12 (UTC)

• 資料

• 上に挙げた [2] の p.5 p.10 p.19 に表があります。黄色が事前条件、水色が事後条件。
• [3] 表でなく箇条書きの形。同じ Eiffel のサイトだがこちらは正しい。
• [4]

これらと 問題の [5] の表の下段の ( ) 内 "Satisfy precondition", "From postcondition" が合っていないことがわかりますね。

• Poshnegevさんがどのように勘違いしているのかを推測しきるのは難しいですが、上の訳文が変なところから見て、 「what the supplier must do (assuming the precondition was satisfied)」を誤読してそうな感じはあります。 「（事前条件が満たされている前提の下で）サプライヤがしなければならないこと」、つまり サプライヤの義務ですね。 なので サプライヤの義務（左下）のところに postcondition と書かれるべきですが、問題の表では precondition と書かれている（のでおかしい）。

--RnTkm（会話） 2021年11月11日 (木) 15:50 (UTC)

(Poshnegev氏が自分の過去の発言を書き換えたのを戻す) RnTkm（会話） 2021年11月11日 (木) 22:56 (UTC)

返答です

• [6]の図表での、黄色はメソッド外部、水色はメソッド内部、です。事前/事後の色分けではありません。

[7]の箇条書きは、The Contract for a Routine（ルーチンのための契約）章節のものなので、ここでは事前条件＝メソッドのrequire、事後条件＝メソッドのensureになります。文脈をはき違えています。

• The client's benefits are outlined in the postcondition. 顧客の利益は事後条件＝ensureで概要されている。
• The client's obligations come from the precondition. 顧客の義務は事前条件＝requireから来る。引数チェックのこと。
• The supplier's obligations are in the postcondition. 業者の義務は事後条件＝ensureになる。
• The supplier's benefits come from the precondition. 業者の利益は事前条件＝requireから来る。require通りの引数でないならメソッド実行しなくてよくなるので。

The client's benefit, which describes what the supplier must do (assuming the precondition was satisfied), is called a postcondition.は（業者がなすべきこと（顧客の事前条件が満たされたと仮定して）を記述している顧客の利益は、事後条件と呼ばれる）としか読めない英文です。

assuming the precondition was satisfiedは、The client's benefitの主格関係代名詞の節内なので、the preconditionは顧客の事前条件を指してます。

正直、そちらの英文解釈にはかなりの誤解があるように見えます。

--Poshnegev（会話） 2021年11月11日 (木) 17:01 (UTC)

@Poshnegev:

• > 上に挙げた [2] の p.5 p.10 p.19 に表があります。

> [6]の図表での、黄色は

文字で 左下のマスに postcondition、右下のマスに precondition と書いているでしょう。

• > [7]の箇条書きは、The Contract for a Routine（ルーチンのための契約）章節のものなので～

「文脈をはき違えています」というのは Poshnegev氏が何を言おうとしているのかよくわかりませんが。

もしかすると、「クラスの契約」と「ルーチンの契約」では違うと言いたいのでしょうか？

「ここでは事前条件＝メソッドのrequire、事後条件＝メソッドのensureになります」

　↑こう書かれているところから推測すると、 ここで言う事前条件・事後条件 以外にも、事前条件・事後条件という名前の(別の)概念があると考えているのでしょうか。そうであれば、その概念の根拠となる文献を示してください。

• 普通の理解では、事前条件・事後条件は メソッド (abstractなものも含む) やサブルーチンについて定めるものだし、記事で書かれるべきものもそれです。 論文 Applying “Design by Contract”でも事前条件・事後条件は ルーチン（メソッド）に対して定めるものとして書かれています。

Poshnegev氏が記事に書いているような、 双方の義務を事前条件、双方の利益を事後条件 と言うような用語法は、（問題の1か所の表を除いては）どこにも書かれていません。 --RnTkm（会話） 2021年11月12日 (金) 06:02 (UTC)

御指摘を反映するように、本文を修正してみました。

--~~~~--Poshnegev（会話） 2021年11月12日 (金) 08:39 (UTC)

@Poshnegev:

　一応言っておきますが、2種類の概念ないし用語法があると私が主張したのではないですよ。あなたの考えを推測したのです。

　そもそも件の文書は Eiffelのチュートリアルであり、契約の概念を説明して終わりではなく、当然 Eiffelのコードをどう書くかという話につなげるでしょう。 実際、問題の表がある節のすぐ次 §Expressing assertions で こう書いていますね。

> Eiffel provides syntax for expressing preconditions (require), postconditions (ensure) and …

ここでは事前条件をrequire、事後条件をensureに対応させている。

　同じ名前で2種類の概念があると見るなら： 初心者向けのチュートリアルの中で、事前条件・事後条件という名前の何らかの概念を説明してから、その直後に 同じ言葉で別の意味を表した（説明や注意、何の断りもなく）、ということになる。 そんなわざと混乱させるような説明をするということがあると思いますか？

　そう考えるよりも、「義務が事前条件、利益が事後条件」という読み方を捨て、表のカッコ内は 意図せず書き間違った（おそらくコピペしてから修正忘れ）ものと解釈した方が 無理がないと思いますよ。

　付け加えて言うと、「義務が事前条件、利益が事後条件」という対応と考えるのは ホーア論理の事前条件・事後条件の意味からも外れると思います。 --RnTkm（会話） 2021年11月13日 (土) 13:33 (UTC)

「事前条件/事後条件」「require/ensure」「義務/利益」の三項目は、どちらがどちらとイコールというものではないようです。それに沿った本稿の修正をいたしました。

メイヤーの講義資料の図表の記述と、eiffel.orgの図表の記述の違いについては、それぞれの状況における三項目の相関性の解釈の違いであり、本質的または基底的な部分での変わりはないので、文章的な表現の違いとして受け止めても特に問題はないと考えます。つまりどちらも間違っている訳ではないということになります。--Poshnegev（会話） 2021年11月14日 (日) 12:15 (UTC)

@Poshnegev:

Wikipedia はあなたのコロコロ変わる自説を記事に書く場ではありません。

出典を手掛かりに推測で組み立てられた概念を書くことは許されていないし（WP:NOR）、そのような推測を断言の形で書くのはなおさらダメです。「ようです」と言っている辺り、推測ということは自分で認めていますね。

「本質的または基底的な部分での変わりはない」←これはあなたの勝手な考えです。誰も同意しませんよ。

・ 問題のチュートリアルのページは、 あなたの読み方でいくなら重大な説明不足があることになるし、私の読み方をするなら書き間違いがあることになる。つまり、どちらの読み方でも かなり重要なところに問題があることになるので、（事前条件・事後条件についての）出典にするには信頼性が低いと言わざるを得ない。

・ あなたが唯一の根拠としている件のページの表は、（仮に内容が正しいとしても） 事前条件・事後条件 という言葉が何であるかを説明するような書き方には そもそもなっていない。そのような記述だけで「サプライヤに義務を課すことを含む 事前条件」なる概念が説明されている、と言い張るのは無理です。

　件のページは、読み方によっては あなたの言うような考えを ほのめかしている と取れるかもしれない、が その程度では根拠として全く足りません。

従って、今の状態ではマトモな出典は提示されていない、削除されても文句は言えません。 --RnTkm（会話） 2021年11月15日 (月) 07:30 (UTC)

コロコロ変えてはいません。OOP風に言えば汎化から特化であり、動物→ネコ科→猫→黒猫という感じです。記述内容の概形は当初から特に変わりありません。先方からの御指摘でより詳細にする機会を頂いてます。eiffel.orgと、そちらの提示資料（これは取って付けの出典になるので記載しませんでしたが）などをよく読めば分かることだと思います。ただ書き過ぎた（特化）部分もあったので一部修正（汎化）いたします。

なお、eiffel.orgは各ページ右上でversion更新が明示されており放置されてる訳ではありません。専門サイトの図表の方が間違いだと即座に断定できるそちらの姿勢の方が問題ではありませんか？　それこそ根拠を示してくれという話になります。先日のorgの図表とその下の文章が合っていないという御指摘も有り体に言えば読み込み不足でしたし、それではただの水かけ論になりかねません。コロコロ変えるよりも、むしろ何があっても考えを変えない方が問題だと考えます。--Poshnegev（会話） 2021年11月15日 (月) 09:15 (UTC)

@Poshnegev:

一応言っておきますが、私は「サイトが間違いだと決めつけた議論」はしていません。 Poshnegev氏の編集が Wikipedia の方針から外れていることを問題にしています。

• まず前提として、Wikipedia:検証可能性 にあるように、

> 信頼できる情報源を欠く編集は、除去されるのもやむを得ません。

記事から記述を除去するのに「記述内容が間違いである」という証拠を示す必要はありません。

また、（信頼できる情報源を材料としたものであっても）独自研究 自体には信頼できる情報源がないと見なされます。（WP:V#他の原則との兼ね合い）

• 件のページの最初の節を 文字通りに読むなら、

「クライアントの義務 は 事前条件と呼ばれる」とは書いているが、

「サプライヤの義務 も 事前条件と呼ばれる」とは書かれていない。

表については、「～を XX と呼ぶ」とか「XX とは、」のような定義文の形にはなっていない。

なので、（表が書き間違いではないと考えるなら、）この節は、 事前条件 という言葉の定義、概念の説明としては不明瞭ということになる。

あなたはたぶん、「サプライヤの義務 も 事前条件と呼ぶ」と解釈しているのだろうけど、それははっきり書かれていることではない。 その上、その解釈は 同ページの後続の節の記述とも相性が悪い。

こういう不明瞭なところをあなたが推測・類推・仮説形成などで勝手に補っているから独自研究 なのです。

WP:OR より:　情報源によって直接的かつ明示的に支持されない観点を～

その足りない部分が他の文献で補われているならまだいいが、あなたはそれもしていない。

• [補足: 上の話だけでも十分だが、同ページの後の節で “クライアントの事前条件”のような書き方がされておらず 単に「事前条件」と書かれていることも Poshnegev氏の解釈を疑う材料になります。　また、Poshnegev氏の言うような「事前条件」概念が 論文 Applying “Design by Contract”に載っていないことも、疑う材料になります。]

• 以上から、件のサイトを出典として 事前条件という概念にサプライヤの義務も含む ように書くのは独自研究と見なされ、これ自体には信頼できる情報源がなく、除去の対象となります。

（「△△のサイトは～～のような記述を載せている」といった書き方だったらまだ許容される可能性はある。） --RnTkm（会話） 2021年11月16日 (火) 16:38 (UTC)

契約による設計は事前条件・事後条件の用語の通り、ホーア論理をベースにしています。事前事後条件への認識のズレがある限り、水掛け論になるのでここで整理しますが、そもそも事前事後条件とは、数学の制約やプログラミングの制約に相当しているものです。プログラミングでの制約とは、集合（ドメイン）と個体（具体的な値）の中間全般を指している要素です（論理プログラミングによく出ます）。整数型付け値xをドメインとすると、x>5は制約になります。xがオブジェクトの場合の制約は、複数の属性への有効範囲指定からずっと複雑になります。

事前事後条件はプログラム上の概念であり、それをソースコードに投影する書式がrequire・ensureと呼ばれます。requireはassert(x >= 0)、ensureはassert((res * res) <= x && (res+1) * (res+1) >= x)のようなコード記述になります。前提記述だけで済む数式とは違って、プログラムでは各実行プロセスでそれらの前提状態に持っていく必要があるので、そのプロセスがクライアントへの義務と形容されており、そこから事後状態に持っていくプロセスがサプライヤへの義務と形容されてます。そのプロセスが正常終了したことを便宜上クライアントの利益と呼び、メソッド未実行になったことを便宜上サプライヤの利益と呼んでいる訳です。

前述のメイヤー講義資料の図表についても、図表の黄色はクライアント側（メソッド外）ルーチンを意味しており、水色はサプライヤ側（メソッド内）ルーチンを意味しています。その黄色に事前条件・クライアント義務・サプライヤ利益が重ねられており、水色に事後条件・サプライヤ義務・クライアント利益が重ねられてるだけで、つまりそのルーチン上で実現されるという意味です。

本稿は、事前条件という概念にサプライヤの義務も含むという意図では書かれていません。それは読み間違えです。「事前条件」と「・サプライヤの義務」のカラム位置が同じになっている通り（インデントしていない）時系列的に並べて書いてるだけです。事後条件を満たすメソッドの正しいコード実装というサプライヤの義務は、事前条件を満たすクライアントの義務と同様にメソッド実行前になされることだからです。--Poshnegev（会話） 2021年11月17日 (水) 09:01 (UTC)

本項目に出現するブロック破りユーザーについて

本項目は、無期限ブロックユーザー利用者:Goldensundown2が始祖とみられるソックパペットが活発に編集していたページになります。

本ユーザーの問題点は、下記の会話ページに記載されているように、出典無し記事の書き増しと、履歴不継承が主なところですが、再三の指摘にも改善がみられないため無期限ブロックとなっています。

また、無期限ブロック中にも多重アカウントによるブロック破りを数度行なっており、周囲に気付かれにくくするために、該当ページで活動中のユーザー名にアカウント名を似せてなりすましを行なう可能性も指摘されています。

• 利用者‐会話:Goldensundown2
• 利用者‐会話:つもりやもり
• 特別:投稿記録/2400:4051:9A1:F00:0:0:0:0/64 (IP範囲は1年間の部分ブロック)
• 利用者‐会話:RnTknn （注: RnTkm とは別人）
• 利用者‐会話:Sycgln
• 利用者‐会話:Transient-account-21515

当該無期限ブロックユーザーは、ブロック破りを常習としており、今後も本ページ並びに周辺技術のページに出現する可能性は非常に高いと思われます。

ブロック破りについては、現在複数人が関心を寄せており、上記ユーザーに似た傾向(出典無し記事の書き増し、履歴不継承)が見られる場合、ユーザーについてのコメント依頼〜投稿ブロック依頼をすることになると思います。--G000001（会話） 2021年11月13日 (土) 13:54 (UTC) G000001（会話） 2021年11月13日 (土) 13:54 (UTC) 　(注意書き追加) RnTkm（会話） 2021年11月14日 (日) 13:18 (UTC)

• 情報: 一連のソックパペット/ブロック破りユーザーについて、現在コメント依頼を出しています。 G000001（会話） 2021年11月24日 (水) 14:59 (UTC)