まず第一に、これは副作用のないアルゴリズムでのみ可能ですか?
第二に、このプロセス、良い本、記事などについてどこで学べますか?
質問する
4925 次
11 に答える
3
通常、正しさの証明は、手元のアルゴリズムに非常に固有のものです。
ただし、使用および再利用されるよく知られたトリックがいくつかあります。たとえば、再帰アルゴリズムでは、ループ不変条件を使用できます。
もう 1 つの一般的なトリックは、元の問題を、アルゴリズムの正しさの証明がより簡単に示せる問題に減らしてから、より簡単な問題を一般化するか、より簡単な問題を元の問題の解決策に変換できることを示すことです。ここに説明があります。
特定のアルゴリズムを念頭に置いている場合は、一般的な答えではなく、そのアルゴリズムの証明を構築する方法を尋ねる方がよい場合があります。
于 2010-01-27T19:06:25.487 に答える
1
LISPに精通している場合は、ACL2を必ず確認してください。http ：//www.cs.utexas.edu/~moore/acl2/acl2-doc.html
于 2010-02-04T01:30:28.180 に答える
1
Elazar がコメントでデモ ビデオを提案しているツールFrama-Cは、関数コントラクトを記述するための仕様言語ACSLと、C 関数がそのコントラクトと実行の不在などの安全性プロパティを満たしていることを検証するためのさまざまなアナライザーを提供します。 -時間エラー。
拡張チュートリアルACSL by exampleでは、実際の C アルゴリズムの指定と検証の例を示し、副作用のない関数と効果的な関数を分けています (副作用のない関数はより簡単であると見なされ、チュートリアルの最初に表示されます)。 . このドキュメントは、記述されているツールの設計者によって書かれたものではないという点でも興味深いので、これらの手法についてより新鮮で教訓的な見方を提供します。
于 2010-01-28T20:36:32.320 に答える
1
Huth と Ryan による Logic in Computer Science は、システムを検証するための最新のシステムの概要を読みやすく説明しています。むかしむかし、人々はプログラムが正しいことを証明することについて話しました - プログラミング言語には副作用があるかもしれないし、ないかもしれません。この本や他の場所から得た印象は、実際のアプリケーションは異なるということです。たとえば、プロトコルが正しいこと、チップの浮動小数点ユニットが正しく除算できること、リンクされたリストを操作するためのロックフリー ルーチンが正しいことなどです。
ACM Computing Surveys Vol 41 Issue 4 (2009 年 10 月) は、ソフトウェア検証に関する特集号です。「Formal Methods: Practice and Experience」で検索すると、ACM アカウントがなくても少なくとも 1 つの論文にアクセスできるようです。
于 2010-01-27T20:16:23.090 に答える
0
WRT (1) では、おそらく、そのような状態ベースの副作用をモデル化することを目的としたプログラム変数でアルゴリズムの副作用を「キャプチャ」する方法で、アルゴリズムのモデルを作成する必要があります。
于 2014-07-21T04:22:33.360 に答える
0
スタンフォードの連中によって開発された PVS ツールは、仕様および検証システムです。私はそれに取り組み、定理証明に非常に役立つことを発見しました。
于 2013-10-16T20:28:32.533 に答える