問題タブ [post-conditions]

この関数では:

事後条件は実行されません (少なくとも、アサーション エラーは発生しません)。私は今、それがそうあるべきだったことを知っています:

実際、これは正しく機能します。

問題は、これが黙って失敗したことであり、何が問題なのかを理解するのにしばらく時間がかかりました. 構文エラー、実行時例外はありません。

Clojure が文句を言わなかった理由を理解するために、Clojure がこのコードで何をするのかを理解したいと思います。 マクロ展開？破壊？角括弧が表示されない場合、コードは消えますか?

誰かがこの質問に答えるのを手伝ってくれるかどうか疑問に思っていました. これは以前の試験用紙からのものであり、今年の試験の準備ができている答えを知っていればできることです。

この質問は非常に単純に思えて、完全に道に迷ってしまいます。正確には何を求めているのでしょうか?

整数変数を含むコードの次のセクションを検討してください。

適切な出力条件を記述し、コード片の正確性を検証することにより、実行後に m が i と j の最小値に等しいことを証明します。

私は投稿条件を次のように持っています: {m = i ∧ i < j ∨ m = j ∧ j < i}

これは正しいです？そして、これをどのように確認しますか？

クラス メソッドの JML 事後条件に、別のメソッド呼び出しへの呼び出しを含めることができますか

たとえば、私はこのクラスを持っています:

doB の事後条件については、次のものを使用できensures doA(x) = doA(y)ます。

Design by Contractアプローチに興味があります。それらを強制するには、preconditionsチェック済み例外を使用する必要があるようです。
しかしpost-conditions、私はそれが好ましいclass-invariantsと思います。 私は正しいですか？私が正しければ、無効にされる可能性のある forおよびアサーションが許可されるのはなぜですか? 事後条件と不変条件も強制するべきではありませんか?assertions
post-conditionsclass-invariants

以下に、gcd メソッドの前後の条件を示します。

ただし、投稿条件をたどるのに問題があります...私にとっては、基本的に、両方で割り切れる整数を見つけると言っています。どのようにして最大除数を取得しますか、実際に条件は何を言っていますか?

コレクション「col」の最大値を見つけるために、前後の条件を記述しようとしています。再帰的にそれを行う方法がよくわからないので、誰かが助けてくれるかどうか疑問に思っていました!

親愛なる専門家や愛好家、

次の問題を解決したいと思います。自然数の配列があります。それらの最大値を見つけたいと思います。

しかし、私はそのような構造図で私の解決策を示さなければなりません http://www.testech-elect.com/pls/images/casetool2.jpg

これは、合計アルゴリズムをmidifieすることで行う必要があります。つまり、http：//cfhay.inf.elte.hu/~hurrycane/programozas/programming_theorems.pdfの構造図と事後条件をmidifieする必要があります。

メインの水平線は維持する必要がありますが、それ以外はすべて変更できます。再帰なしで変更された事後条件を教えてください。それで十分でしょう。構造図がわかれば作れます。前もって感謝します。

パブリック メソッドの事前条件と事後条件は、このメソッドとそのクライアントの間の契約を形成します。

1.によると、呼び出し元は事後条件を検証してはならず、呼び出されたメソッドは事前条件を検証してはなりません:

プログラム 49.2 に示すように、平方根関数 sqrt の事前条件と事後条件を思い出してください。sqrt を呼び出す関数は、負でない数値を関数に渡す必要があります。負の数が渡された場合、平方根関数はそれを処理するために何もしません。一方、負でない数値が sqrt に渡された場合、事後条件を満たす結果を返すのは sqrt の責任です。したがって、sqrt の呼び出し元は、結果を確認または修正するために何もする必要はありません。

操作の事前条件が失敗した場合、呼び出し元を非難する 操作の事後条件が失敗した場合、呼び出された操作を非難する

しかし、別の記事に含まれるコードに見られるように、呼び出されたメソッドは前提条件を検証します:

a)メソッド の前提条件を満たすことはクライアントの責任であるため、呼び出されたメソッドも前提条件が満たされているかどうかを確認する必要がありますか?

b)事後条件を満たす結果を提供するのは呼び出されたメソッドの責任であるため、呼び出し元は事後条件をチェックする必要がありますか?

2.最初の記事で述べた利点の 1 つは、「事前条件と事後条件を使用して、OOP のクラス間で責任を分割できる」ことです。これは、呼び出されたメソッドが前提条件を検証する責任を負わないことも理解しています。 postconditionを検証する呼び出し元の責任ではありません。

しかし、そのような哲学に固執すると、コードがより脆弱になるのではないでしょうか? コードは相手 (呼び出し元またはメソッドのいずれか) が約束を果たすことを盲目的に信頼するからです。

3.呼び出し元/呼び出されたメソッドが相手を盲目的に信頼していない場合、事後条件と事前条件によって提供される利点の多くを失うことはありません。これは、呼び出されたメソッドが前提条件もチェックする責任を負い、呼び出し元が責任を負う必要があるためです。事後条件を確認するには？

ありがとう

編集

3.

呼び出し元/呼び出されたメソッドが other party を盲目的に信頼していない場合、事後条件と事前条件によって提供される利点の多くを失うことはありません。これは、呼び出されたメソッドが前提条件もチェックする責任を負い、呼び出し元が検証する責任を負う必要があるためです。事後条件？

事後条件は呼び出されたメソッドによって保証される必要があるため、呼び出し元は事後条件を検証する必要はありません。コントラクトを強制する他の方法がないため、呼び出されたメソッドは前提条件を確認する必要があります。

a)事後条件は、戻り値が指定された型であること、またはnull( 戻り値がnullableの場合)であることのみを述べる/保証する必要があると想定していますか? 戻り値がどのタイプになるかの他に、戻り値が指定された範囲内にあるかどうかなど、他のことを事後条件で指定することはできません(これは type system では検証できません) (例:事後条件でその戻り値を指定することもできません)の範囲内になります)? この場合、クライアントはpostconditionもチェックする必要があるのではないでしょうか?int10-20

b) それでは、最初の記事は、呼び出されたメソッドが前提条件をチェックしてはならないという主張が間違っていると言えますか?

2.編集

いいえ、事後条件は null チェックだけでなく、何でもかまいません。どちらの方法でも、クライアントは事後条件が検証済みであると想定できるため、たとえば、契約で保証されていると記載されている場合、int 範囲を検証する必要はありません。

a) 以前、コードの脆弱性を軽減するために、呼び出されたメソッドによって事前条件をチェックする必要があると述べましたが、呼び出し元が事後条件を検証する必要があることも理由にできませんでした(たとえば、返された値が事後条件によって約束された範囲内にあることを検証します)呼び出し元のコードの脆弱性を軽減するには?int

b）クライアントが事後条件によって行われたクレームを盲目的に信頼できる場合（事後条件が戻り値がある範囲内にあるなどのクレームを作成する場合、それは盲目的な信頼だと思います）、呼び出されたメソッドも、呼び出し元が呼び出されたメソッドの前提条件を満たすことを信頼できないのはなぜですか？