問題タブ [formal-verification]

ポイントが長方形の内側にあるかどうかをチェックする次のアルゴリズムが有効かどうか疑問に思いました。私は自分の直感を使ってそれを開発しました（それをサポートするための強力な三角法/数学の基礎はありません）ので、この問題についてより多くの経験を持つ誰かから聞いてみたいです。

コンテクスト：

• 長方形は4点で定義されます。回転させることができます。
• 座標は常に正です。
• 定義上、点は長方形と交差する場合、長方形の内側と見なされます。

仮説：

• ポイントと長方形の頂点の間の距離を使用します（下の最初の図）。
• 可能な最大合計距離は、ポイントが1つの頂点にある場合です（2番目の図）。
• ポイントが長方形のすぐ外側にある場合、距離は大きくなります（3番目の図）。

図のリンク： http： //i45.tinypic.com/id6o35.png

アルゴリズム（Java）：

質問：これは正しいですか？

CQRS は、すぐに一貫性のあるモデルの事後条件をどのように処理しますか? このようなことは、イベント ソーシングなどを使用した最終的に一貫性のあるシステムでは無関係であることに気付きました。しかし、バニラ CQRS を単純なインターフェイスに適用したいだけの場合、事後条件をどのように記述すればよいでしょうか? CQRS の考えは常に結果整合性を前提としていますか?

クラッド:

CQRS:

信号の 2 つのパック配列があり、特定の条件下で 2 つの配列が同一であることを証明するプロパティとそのプロパティに関連付けられたアサーションを作成する必要があります。私は正式に検証していますが、ツールは 1 つのプロパティで両方の完全な配列を証明できないため、個々の要素に分割する必要があります。ループを使用して配列の各要素のプロパティを生成する方法はありますか? 現時点では、私のコードは非常に冗長でナビゲートが困難です。

私のコードは現在次のようになっています。

これは、コードを次のようにしたい場合の一種です。

定理証明ツールz3は、数式を解くのにかなりの時間がかかります。これは、簡単に処理できるはずです。これをよりよく理解し、おそらくz3への入力を最適化するために、z3が解決プロセスの一部として生成する内部制約を確認したいと思いました。コマンドラインからz3を使用する場合、バックエンドソルバー用にz3が生成する数式を出力するにはどうすればよいですか？

私がこのような関数を持っているとしましょう：

この些細な関数は常に1を返します。-O2オプションを指定してclangを使用してコンパイルし、分解されたコードを見ると、LLVMはこの関数を。として正しくコンパイルしますreturn 1;。

私の質問は：llvmは静的値analysysをどのように実行しますか？最も弱い前提条件のテクニック？値の伝播？ホアのテクニック？

プログラムのプロパティを検証するためのさまざまな正式な検証ツールがあることを認識しています (たとえば、SPIN モデル チェッカー)。リアルタイム組み込みシステムのタイミング要件を検証するための一般的なツール/方法はありますか? 例: 「このアルゴリズムは常に 50 ミリ秒以内に終了する必要があります」。この種の検証は通常どのように行われますか?

Daniel Jackson の優れた本 ( Software Abstractions)の例、具体的にはリーダーを選出するために彼がトークンリングをセットアップしている例に従っています。

この例 (リング選挙) を拡張して、トークンが 1 つに限定されるのではなく、指定された時間内にすべてのメンバーに渡されるようにしようとしています (各メンバーは複数回ではなく 1 回だけ選出されます)。ただし (主に合金の経験が浅いため)、最善の方法を見つけるのに問題があります。最初は、いくつかの演算子 (- を + に変更) をいじれると思っていましたが、うまくいきませんでした。

以下は、例のコードです。私は質問でいくつかの領域をマークアップしました...すべての助けに感謝します。アロイ4.2を使用しています。

弱い順序の同時実行を実験するのに役立つツールは何ですか? つまり、パーシャル フェンス、弱いアトミック、取得/消費/解放セマンティクス、ロックフリー アルゴリズムなどについて学習しながら、どのサンドボックスでプレイできるでしょうか?

必要なツールまたはサンドボックスは、アルゴリズムが理論的に失敗する可能性のあるさまざまな方法を明らかにして、弱く順序付けられたスレッド化されたアルゴリズムを実行および強調します。たとえば、x86 上で物理的に実行されている場合でも、このツールは ARM タイプの障害を公開できます。

オープンソースのツールが望ましいでしょう。お知らせ下さい。

参考文献:

• C++11 ドラフト標準(PDF、条項 1、29、および 30 を参照)。
• ハンス-J. 主題のベームの概要。
• この件については、マッケニー、ベーム、クロール。
• この件に関するGCCの開発ノート;
• この件に関する Linux カーネルのメモ。
• Stackoverflow に関する回答付きの関連する質問
• 別の質問です。これはフェンスとアトミックを比較するものです。
• Cppmem (@KerrekSB のアドバイスによる);
• Cppmem のヘルプ ページ;
• Spin (@JohnZwinck のアドバイスによる、並行システムの論理的一貫性を分析するためのツール)。

(参照は C++11 に向けられています。なぜなら、これがたまたまこのテーマにアプローチしたからです。しかし、私が知る限り、C++ 以外の回答が最善かもしれません。フィット。）

Cadence Incisive FormalVerifierを64ビットモードで実行できるかどうか知っていますか？