58

大学で形式的なシステムについて教わりましたが、実際には使われていないようで残念でした。

私は、テストではなく証明によって、コード (オブジェクト、関数など) が機能することを知ることができるという考えが好きです。

私たちは皆、物理工学とソフトウェア工学の間に存在しない類似点に精通していると確信しています (鉄は予測通りに動作し、ソフトウェアは何でもできます - 誰にもわかりません!)。実際に使用することができます (Web フレームワークを求めるのは多すぎますか?)

scala のような関数型言語のテスト可能性について興味深いことを聞いたことがあります。

ソフトウェアエンジニアとして、どのような選択肢がありますか?

4

11 に答える 11

39

はい、確かに正しいソフトウェアを書くために設計された言語があります。業界で使用されているものもあります。Spark Adaはおそらく最も顕著な例です。Praxis Critical Systems Limited の何人かと話をしたところ、Boings で実行するコード (エンジンの監視用) にそれを使用していましたが、非常に優れているようです。(ここに、言語の優れた要約/説明があります。) この言語と付随する証明システムは、以下で説明する 2 番目の手法を使用します。動的メモリ割り当てもサポートしていません!

私の印象と経験によると、正しいソフトウェアを書くには 2 つのテクニックがあります。

  • 手法 1: 使い慣れた言語 (C、C++、Java など) でソフトウェアを作成します。そのような言語の正式な仕様を取り、あなたのプログラムが正しいことを証明してください。

    あなたの野望が 100% 正しいこと (自動車/航空宇宙産業で最も頻繁に要求されること) である場合、プログラミングに費やす時間はほとんどなく、証明により多くの時間を費やすことになります。

  • テクニック 2: 少しぎこちない言語 (たとえば、Ada の一部のサブセットまたは OCaml の微調整バージョン) でソフトウェアを書き、途中で正当性の証明を書きます。ここでは、プログラミングと証明が密接に関連しています。Coq でのプログラミングは、それらを完全に同一視することさえあります! (カリー・ハワード通信を参照)

    これらのシナリオでは、常に正しいプログラムになります。(バグは仕様に根ざしていることが保証されます。) プログラミングにより多くの時間を費やす可能性がありますが、その一方で、途中でそれが正しいことを証明しています。

両方のアプローチは、正式な仕様が手元にあるという事実 (他にどのように正しい/正しくない動作を伝えるか) と、正式に定義された言語のセマンティクス (実際の動作が何であるかを他にどのように伝えることができるか) に依存していることに注意してください。あなたのプログラムのです）。

正式なアプローチの例をさらにいくつか示します。それが「現実世界」であるかどうかは、誰に尋ねるかによって異なります:-)

私が知っている「証明可能で正しい」Web アプリケーション言語はURだけです。「コンパイラを通過する」Ur プログラムは、次のことが保証されていません。

  • あらゆる種類のコードインジェクション攻撃に苦しむ
  • 無効な HTML を返す
  • 無効なアプリケーション内リンクを含む
  • HTML フォームとそのハンドラーが期待するフィールドとの間に不一致がある
  • リモート Web サーバーが提供する「AJAX」スタイルのサービスについて誤った仮定を行うクライアント側コードを含める
  • 無効な SQL クエリを試行する
  • SQL データベースとの通信、またはブラウザーと Web サーバーとの間の通信で、不適切なマーシャリングまたはアンマーシャリングを使用する
于 2010-10-31T21:13:41.020 に答える
24

この質問に答えるには、「証明可能」とは何かを定義する必要があります。Ricky が指摘したように、型システムを備えた言語は、プログラムをコンパイルするたびに実行される組み込みの証明システムを備えた言語です。これらの証明システムはほとんどの場合、悲しいことに無力です — Stringvsのような質問にInt答え、「リストはソートされていますか?」のような質問を避けます。—しかし、それらは証明システムです。

残念なことに、証明の目標が高度になればなるほど、証明をチェックできるシステムで作業することが難しくなります。これは、チューリング マシン上で決定不能なクラスの問題の規模を考えると、すぐに決定不能にエスカレートします。確かに、ソート アルゴリズムの正確性を証明するなどの基本的なことは理論的には実行できますが、それ以上のことは非常に薄い氷の上を踏むことになります。

ソート アルゴリズムの正しさのような単純なことを証明する場合でも、比較的高度な証明システムが必要です。(注: 型システムが言語に組み込まれた証明システムであることは既に確立しているので、私はもっと力強く手を振るのではなく、型理論の観点から物事について話します)リストの並べ替えの完全な正当性の証明には、何らかの形式の依存型が必要です。そうしないと、型レベルで相対値を参照する方法がありません。これは、決定不可能であることが示されている型理論の領域にすぐに侵入し始めます。したがって、リストの並べ替えアルゴリズムの正しさを証明できるかもしれませんが、それを行う唯一の方法は、検証できない証明を表現できるシステムを使用することです。個人的には、

先ほど触れた使いやすさの面もあります。型システムが洗練されればされるほど、使い心地は悪くなります。これは厳格なルールではありませんが、ほとんどの場合、当てはまると思います。また、他の正式なシステムと同様に、最初に実装を作成するよりも、証明を表現する方が手間がかかる (そしてエラーが発生しやすい) ことがよくあります。

以上を踏まえて、Scala の型システム (Haskell の型システムと同様) がチューリング完全であることは注目に値します。つまり、理論的にはそれを使用して、コードに関する決定可能なプロパティを証明することができます。そのような証明に適している方法。Java よりも Haskell の方が優れた言語であることはほぼ間違いありません (Haskell の型レベル プログラミングは Prolog に似ているのに対し、Scala の型レベル プログラミングは SML に似ているため)。Scala や Haskell の型システムをこのように使用することはお勧めしませんが (アルゴリズムの正しさの正式な証明)、このオプションは理論的には利用可能です。

全体として、「現実の世界」で正式なシステムを見たことがない理由は、正式な証明システムがプラグマティズムの無慈悲な専制政治に屈服したという事実に由来すると思います。前述したように、正当性の証明を作成するには非常に多くの労力が費やされるため、ほとんど価値がありません。業界はずっと前に、あらゆる種類の分析的な正式な推論プロセスを経るよりもアドホックなテストを作成する方が簡単であると判断しました.

于 2010-10-31T22:42:05.690 に答える
10

あなたは、私たちの多くが何年にもわたって尋ねてきた質問をしています。良い答えがあるかどうかはわかりませんが、ここにいくつかの部分があります：

  • 今日の使用で証明される可能性のある、十分に理解された言語があります。ACL2 経由の Lisp もその 1 つです。もちろん、Scheme にも十分に理解された正式な定義があります。

  • 多くのシステムが、Haskell のような純粋な関数型言語、またはほぼ純粋な関数型言語を使用しようとしました。Haskell ではかなりの数の正式なメソッドが機能します。

  • 20年以上前にさかのぼると、正式な言語のハンドプルーフを使用するための短命のことがあり、その後コンパイルされた言語に厳密に翻訳されました. いくつかの例は、IBM の Software Cleanroom、ACL、Gypsy、Rose out of Computational Logic、John McHugh と私の C の信頼できるコンパイルに関する研究、および C システム プログラミングのハンドプルーフに関する私自身の研究です。これらはすべて注目を集めましたが、どれもあまり実用化されていませんでした。

興味深い質問だと思いますが、形式的なアプローチを実践するための十分な条件は何でしょうか? いくつかの提案を聞きたいです。

于 2010-10-31T21:09:19.917 に答える
9

型付き言語は、特定のカテゴリの障害がないことを証明します。型システムが高度になればなるほど、より多くの障害が存在しないことを証明できます。

プログラム全体が機能することを証明するために、そうです、数学とプログラミングが互いに出会い、握手をしてから、プログラマーがギリシャ記号を処理できない方法についてギリシャ記号を使用して話し始める、通常の言語の境界の外に足を踏み入れています。とにかく、それはそれのΣについてです。

于 2010-10-31T21:00:08.530 に答える
4

私は 2 つの証明可能な言語に携わっています。1 つ目は、Perfect Developer がサポートする言語です。これは、ソフトウェアを指定して改良し、コードを生成するためのシステムです。PD自体を含むいくつかの大規模システムに使用されており、多くの大学で教えられています。私が関与している 2 番目の証明可能な言語は、MISRA-C の証明可能なサブセットです。詳細については、C/C++ 検証ブログを参照してください。

于 2011-02-10T01:50:57.253 に答える
4

オメガをチェックしてください。

この紹介には、正確性の証明が含まれている AVL ツリーの比較的簡単な実装が含まれています。

于 2010-11-01T19:39:18.620 に答える
4

そのような証明可能な言語の現実世界での使用は、あとがきを書いて理解するのが非常に難しいでしょう。ビジネスの世界では、迅速に機能するソフトウェアが必要です。

「証明可能な」言語は、大規模なプロジェクトのコードベースの書き込み/読み取りには対応できず、小規模で孤立したユースケースでのみ機能するようです。

于 2010-10-31T22:50:44.843 に答える
3

Scalaは「現実の世界」であることが意図されているため、Scalaを証明できるようにするための努力はなされていません。Scalaでできることは、関数型コードを作成することです。関数型コードはテストがはるかに簡単です。これは、「現実世界」と証明可能性の間の適切な妥協点です。

編集=====MLが「証明可能」であるという私の誤った考えを削除しました。

于 2010-10-31T22:09:24.210 に答える
3

証明可能な正しいコードのコンテキストにおける「現実世界」の私の（物議を醸す）定義は次のとおりです。

  • ある程度の自動化を伴う必要があります。そうしないと、面倒な小さな詳細を証明して処理するのに非常に多くの時間を費やすことになり、完全に非現実的になります (おそらく宇宙船制御ソフトウェアとその種のことを除いて、あなたが実際には、綿密なチェックに大金を費やしたいと思うかもしれません)。
  • ある程度の関数型プログラミングをサポートする必要があります。これにより、非常にモジュール化され、再利用可能で、推論しやすいコードを書くことができます。明らかに、Hello World やさまざまな単純なプログラムを作成または証明するために関数型プログラミングは必要ありませんが、ある時点で、関数型プログラミングは非常に便利になります。
  • 必ずしも主流のプログラミング言語でコードを書ける必要はありませんが、代替手段として、少なくともコードを主流のプログラミング言語で書かれた合理的に効率的なコードに機械翻訳できる必要があります。仕方。

上記は比較的普遍的な要件です。命令型コードをモデル化する機能や、高階関数が正しいことを証明する機能など、その他の機能は、一部のタスクにとって重要または不可欠な場合がありますが、すべてではありません。

これらの点を考慮すると、私のこのブログ投稿にリストされているツールの多くは役立つかもしれませんが、それらはほとんどすべてが新しく実験的なものであるか、業界のプログラマーの大多数にとってなじみのないものです. ただし、そこでカバーされている非常に成熟したツールがいくつかあります。

于 2012-06-10T12:13:41.440 に答える
3

要件の 1 つが証明可能性である場合に使用される、Haskell などの純粋関数型言語を調べることができます。

関数型プログラミング言語と純粋な関数型プログラミング言語に興味があるなら、これは楽しい読みものです。

于 2010-10-31T21:08:32.190 に答える
2

イドリスとアグダはどうですか？現実世界で十分？

実際の良い例として、Agda で書かれた検証済みの HTTP REST ライブラリを提供することを目的とした Lemmachine というプロジェクトがあります: https://github.com/larrytheliquid/Lemmachine

于 2015-01-27T00:57:51.460 に答える