問題タブ [invariants]

私は、プログラマーがインターフェイスで不変条件 (事前および事後条件) を指定できるようにする Java フレームワークを作成することを考えていました。目的は、コードをより堅牢にし、同じインターフェイスのさまざまな実装に対して記述する必要がある単体テストの数を減らすことです。

私は、プログラマーも書く不変条件でメソッドに注釈を付ける何らかの方法を作成することを想定しています。例えば

実装がソートされたリストを返すことを保証するために、アノテーションで装飾されます。この注釈は、任意の実装に対してコンパイル時に実行できる単体テストにリンクされます。

これはクレイジーなアイデアですか、それともより広いプログラミング コミュニティに役立つでしょうか?

私はAndroidアプリケーションを開発しています。

サイズを次のようにchar配列に設定したいと思います。

しかし、それは機能しません。それを機能させるには、5番目の番号を削除する必要があります。

言語変数を5文字に制限したい。どうやってやるの？

ありがとう。

JML について質問があります。違いは何ですか

そしてそれを次のように宣言します

array_?の要素について それぞれの場合にどのようなプロパティが保持されますか?

前もって感謝します。

仕事中の本のコーダーで、著者は「コードで不変条件をどのように使用しますか」と尋ねます。この質問の意味を説明してください。

wikiでクラスの不変条件を見ましたが、例はJavaであり、この例をC＃に関連付けるのに十分なJavaのスキルがありません。.NET 4.0では、不変性、共変性、反変性が導入されており、ここで詳しく説明されています。不変性はとても広いです。著者による単語の使用法は、単体テストに関連しているようです。その本を読んだ人にとって、著者はどういう意味ですか？仮定を立てて、単体テストの後に妥当性をテストすることについて話しているのでしょうか。

誰かが、共変性、反変性、不変性、および反不変の簡単なC＃の例を提供してくれませんか（そのようなものが存在する場合）。

これまでに見たすべてのサンプルは、何らかのオブジェクトを にキャストしただけでしたSystem.Object。

C ++でクラスの不変条件をチェックするための確立されたパターンはありますか？

理想的には、不変条件は、各パブリックメンバー関数の最初と最後に自動的にチェックされます。私の知る限り、クラス付きのCは特別なメンバー関数を提供してbeforeいafterましたが、残念ながら、契約による設計は当時あまり人気がなく、Bjarne以外はその機能を使用していなかったため、彼はそれを削除しました。

もちろん、check_invariants()各パブリックメンバー関数の最初と最後に手動で呼び出しを挿入するのは面倒でエラーが発生しやすくなります。RAIIは例外を処理するための最適な武器であるため、不変チェッカーを最初のローカル変数として定義する次のスキームを考え出しました。不変チェッカーは、構築時と破棄時の両方で不変条件をチェックします。

質問＃0：名前のないローカル変数を宣言する方法はないと思いますか？:)

コンストラクタの最後とデストラクタの最初check_invariants()で手動で呼び出す必要があります。ただし、多くのコンストラクタボディとデストラクタボディは空です。その場合、最後のメンバーとしてを使用できますか？FooFooinvariants_checker

質問1：オブジェクトがまだ作成中であっても、そのポインターを介してすぐに呼び出すコンストラクターに渡すthisことは有効ですか？invariants_checkercheck_invariantsFoo

質問2：このアプローチで他に問題がありますか？改善できますか？

質問3：このアプローチは新しいものですか、それともよく知られていますか？より良い解決策はありますか？

私はホーア論理を見ていますが、ループ不変条件を見つける方法を理解するのに問題があります。

誰かがループ不変条件を計算するために使用される方法を説明できますか？

そして、ループ不変条件が「有用な」ものであるために何を含むべきでしょうか？

私は単純な例だけを扱っており、不変条件を見つけて、次のような例で部分的および完全な修正を証明しています。

次のことを考慮してください

これにより、

だけでなく、「違法」

アリティが引数リストの長さと一致しないため、「不正」です。

このような関数を使用しないと

Predicate モジュールから makePred のみをエクスポートする場合、値コンストラクターの正確性を強制する方法はありますか?

試験のアルゴリズムを改訂していて、この演習を解決しようとしていましたが、解決策を思い付くことができませんでした。

これは擬似コードです。

したがって、特定の入力（たとえば、x=1およびa={0,1,1,1,1}）の場合、14行目で返される値が4行目の事後条件：演習では、次のように求めています。 。ヒント：何が変わらないかを述べるために含めるようにしてください。」

私は解決策を見つけることができませんでした。誰か助けてもらえますか？

よろしくお願いします、VJ

編集：わかりました、あなたの助けてくれてありがとう。

}真ん中を返す;

バリアントをミドルに選択しました。そして不変である：

0x

これは正しいと思いますか？

クラスの不変条件が無効になった場合に備えて、実行時例外をスローしたいと考えています。これはプログラミング エラー (NullPointerException と同様) であるため、クライアントはその例外をキャッチすべきではありません。

例外クラスをプライベートまたはパブリック (またはその他) と宣言する必要がありますか?

カスタムのランタイム例外と可視性に関するガイドラインはありますか?