問題タブ [correctness]

• モデル チェックを使用したアプリケーションの種類は何ですか?
• どのモデル チェック ツールを使用しましたか?
• この手法を使用した経験、特に高品質のソフトウェアを提供する上での有効性を評価した経験をどのように要約しますか?

研究の過程で、 Spinを使用する機会があり、実際のモデル チェックがどの程度行われているか、組織がそれからどれだけの価値を得ているかについて興味をそそられました。私の実務経験では、ロジックに正式な検証を適用することは (当然のことながら) 考慮されていないビジネス アプリケーションに取り組んできました。SO の人々のモデル チェックの経験と、この件に関する考えについて本当に知りたいです。モデル チェックは、ツールキットに含める必要がある、より広く使用される開発プラクティスになるのでしょうか?

最小スパニング ツリー問題は、接続された重み付きグラフを取得し、グラフを接続したまま (結果として非循環グラフが生成される) で、合計重みが最小のエッジのサブセットを見つけることです。

私が検討しているアルゴリズムは次のとおりです。

• すべてのサイクルを見つけます。
• 各サイクルから最大のエッジを削除します。

このバージョンの推進力は、反復的な構造を持たない「ルールの満足」に制限された環境です。また、非常に並列なハードウェア (つまり、サイクル数より数倍の並列度が期待されるシステム) にも適用できる場合があります。

編集:

上記はステートレスな方法で行われます (どのサイクルでも最大のエッジではないすべてのエッジが選択/保持/無視され、その他はすべて削除されます)。

マルチスレッドアルゴリズムは、設計/デバッグ/証明が特に困難です。デッカーのアルゴリズムは、正しい同期アルゴリズムを設計することがいかに難しいかを示す代表的な例です。タネンバウムの最新のオペレーティングシステムは、IPCセクションの例でいっぱいです。誰かがこれについての良い参考文献（本、記事）を持っていますか？ありがとう！

これらのforループは、アルゴリズムの正式な正当性証明の最初の基本的な例の 1 つです。それらには、異なるが同等の終了条件があります。

違いは事後条件で明らかになります。

• i == N最初のものは、ループが終了した後の強力な保証を提供します。

• 2番目のものは、ループが終了した後の弱い保証を与えるだけi >= Nですが、それを仮定したくなるでしょうi == N.

何らかの理由でインクリメント++iが のようなものに変更されたi += 2場合i、またはループ内で変更された場合、またはNが負の場合、プログラムは失敗する可能性があります。

• 最初のものは無限ループに陥る可能性があります。エラーのあるループの早い段階で失敗します。デバッグは簡単です。

• 2 番目のループは終了し、後で間違った仮定のためにプログラムが失敗する可能性がありますi == N。バグの原因となったループから遠く離れた場所で失敗する可能性があり、追跡が困難になります。または、予想外のことを静かに続けてしまうこともあり、これはさらに悪いことです。

あなたはどの終了条件を好みますか、またその理由は何ですか? 他の考慮事項はありますか？これを知っている多くのプログラマーが、なぜそれを適用することを拒否するのでしょうか?

乱数ジェネレーターを使用する場合、これは新しい値のランダム性を高めるために使用するより良い方法です。

1. 毎回 RNG の新しいインスタンスをインスタンス化し、値を返すメソッドがありますか?

2. クラス レベルで RNG のインスタンスがあり、これはコンストラクターで一度インスタンス化され、既存のインスタンスを使用して新しいランダム値の後続のすべての呼び出しが行われますか?

問題は、多くの場合、互いに接続されていない異なるスコープで、乱数の呼び出しが多数ある可能性があることです。

これはパフォーマンスの問題ではないため、各呼び出しが新しいインスタンスをインスタンス化する可能性があるという事実は違いはありません。これはすべて、戻り値のランダム性に関するものです。

問題があり、これを解決する正しい方法を学びたいと思います。

私はデータオブジェクトを持っています

LinkHolder.Text値を説明テキストとして使用するRadioButtonリストをユーザーに提示したいと思います。それからポストバックで、私はしたいです

対応するリンク上。

これを行うための最良/最も正しい方法がわかりません。ヒントをいただければ幸いです。

それをバックアップするための正当性を証明して開発されたシステムやソフトウェアはありますか? それとも、すべての重要なシステムは、積極的なコード レビューとテスト サイクルだけで開発されているのでしょうか?

私たちのグループは、産業プロセスをシミュレートするプロセス モデリング アプリケーションを構築しています。このプロセスの最終出力は、化学物質と流量を表す一連の数値です。

このアプリケーションは、まったく同じ基礎となる数学モデルを使用してシミュレーションを作成する非常に古いソフトウェアに基づいています。シミュレーションには何千もの変数が含まれます。

各コンポーネントは単体テスト済みですが、ソフトウェアによって生成されたデータ出力が古いシミュレーション ソフトウェアのものと一致することを確認できるようにする必要があります。形式化された厳密な方法で、この問題にどのようにアプローチするのが最善かを考えています。

古いプログラムは、テキスト ファイルを介して入力を指定することによって機能するため、プログラムで各変数を取得し、ファイル内の値を調整して (それに応じて新しいアプリケーションでも)、新しいアプリケーションと古いアプリケーションの出力を比較できると考えていました。モデル内のすべての変数に対してこれを行います。

各変数の許容範囲はわかっているので、その特定の変数の正確性を示すには、いくつかの値の各変数のランダム サンプルで十分だと思います。

このアプローチについて何か考えはありますか？他のアイデアはありますか？

以下のようなカウント関数をテストしていた場合、1 つの関数で複数の関数をテストすることと、各テストにテスト関数を使用することは、「正しい」または「間違っている」と見なされますか?

Mavenに、マシンにインストールされているアーティファクトではなく、リモートアーティファクトを使用させる方法はありますか？コンパイルエラーではなくランタイムエラーを心配しているので、ビルドサーバーは有効なオプションではありません。

PS .m2フォルダーを削除または名前変更できることはわかっていますが、これを行うにはもっと賢い方法があるに違いありません。たぶんプラグインや特別なコマンドパラメータ？