問題タブ [post-conditions]

Programming: Principles and Practice using C++ の 5.10.1 章には、領域の不正な入力をデバッグするための "Try this" 演習があります。事前条件は長さと幅の入力が 0 または負の場合で、事後条件は面積が 0 または負の場合をチェックします。問題を引用すると、「このバージョンの領域の事前条件が成立するが、事後条件が成立しないような値のペアを見つけてください。」. これまでのコードは次のとおりです。

コードは機能しているように見えますが、どの入力が成功するための事前条件を取得し、事後条件をトリガーするかについて頭を悩ませることはできません。これまでのところ、入力の1つに文字列を入力しようとしましたが、プログラムを終了し、0に相当するASCIIを検索しようとしましたが、結果も同じでした. これはある種のトリックの質問であるはずですか、それとも何か不足していますか?

だから私はエッフェルプログラミングに不慣れで、特にループを書くことでensure、 a のブロックに事後条件を書くことを学ぼうとしています。feature

だから私はこれを試しました：

しかし、何らかの理由で、 と の不明な識別子を取得しiますj。このエラーの原因と修正方法を知っている人はいますか? また、ブロックで使用across ... as ... all ... endする別の方法はありますか? ensureよろしくお願いします！

このコードの事前条件の意味と目的は理解できますが、事後条件の意味と目的を理解するのに問題があります。このPush部分は、整数をプッシュした後にポインタを増やすことを知っています（ Pointer = Pointer~ +1 ）。このPop部分は、整数をポップした後にポインターを減らすことを理解しています（ポインター=ポインター〜-1）。

メソッドの事前条件と事後条件 (およびクラス不変条件) に基づいて単体テストを自動的に生成するツールがあるかどうか疑問に思います。

正確には、メソッドの事前条件と事後条件 (およびおそらくクラス不変条件) が与えられ、その情報に基づいて単体テストを生成したいとします。この目的のための実用的なツールを探しています。

Korat と TestWizard は知っています。いくつかのテクニック/ツールを挙げていただけますか?

PS: プログラミング言語、またはメソッド コントラクトを指定するために使用する言語は、それほど重要ではありません。知りたいのはテクニックだけです。

ありがとうございました。