問題タブ [formal-methods]

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

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

そう...

私はソフトウェア工学の形式的手法を教えています。「アジャイル方法論」も教えています。ほとんどの人は、これは矛盾していると考えているようです。それは非常に理にかなっていると思います... 私はまた、実際に物事を成し遂げる必要がある会社で働いています :) 獲得したスキルポイントを「仕様」に日常的に適用できますが、私の同僚は通常、「フォーマル」という言葉を避けます。

私は、これは私たちがプログラミング方法を学ぶ本質的な方法によるものだと思っていました。私たちは通常、問題を理解するのではなく、実用的な解決策を見つけるように駆り立てられています。それから、これは正式なコミュニティのほとんどの人がエンジニアではなく、数学者またはコンピューター科学者であるという事実によるものだと思いました。今日では、正式な方法のコミュニティがある種の「難読化」法の背後に隠れて、利用可能なすべての UNICODE シンボルを使用し、失礼で審美的でないツールを積極的に開発し、標準に直面して笑っているからではないかと思います。

はい、私は「彼らを責める」から「私たちを責める」視点に移行しています;-)

では、私の質問は次のとおりです。あなたの会社では、何らかの正式な方法を使用していますか? それらを導入しましたか、それとも前提条件でしたか? 人々の恐怖から数学の霧を取り除き、形式的な方法を使用するように促すために、どのような手法を使用しますか? より一般的な用途において、現在のツールに欠けているものは何だと思いますか?

私たちのクライアントは、ソフトウェア要件を収集するための Web ベースのリッチ インターネット アプリケーションを構築することを望んでいます。基本的には、利害関係者から要件を取得するための特定のプロセスに従う Web ベースのケース ツールです。私はプロジェクト マネージャーで、まだプロジェクトの初期段階にあります。

クライアントと開発者の両方にとってツールの要件を明確にするために、形式的な方法を使用することを考えていました。正式な方法とは、何らかの形のモデリング、おそらく数学に基づくものを意味します。Z ( http://en.wikipedia.org/wiki/Z_notation )、ステート マシン、UML 2.0 (おそらくOCLなどの拡張機能を使用)、ペトリ ネット、およびいくつかのコーディングについて読んだことがあり、検討していることもあります。契約や前後の条件などのレベルのもの。他に考慮すべきことはありますか？

開発者は経験豊富ですが、使用する形式によっては、数学を学ぶ必要がある場合があります。

このプロジェクトで形式的な方法を使用する価値があるかどうか、もしそうならどの程度の価値があるかを判断しようとしています。私は「場合による」ことを知っているので、私にとって最も役立つ答えは、はい/いいえとそれを裏付ける議論です。

あなたがこのプロジェクトに参加した場合、正式な方法を使用しますか?

これは一種の奇妙な質問です。形式手法を使ったプログラミングの学習に関する本を書いている最中です。プログラミングの経験がある人を対象にしています。アイデアは、彼らに高品質のプログラマーになるように教えることです。

基本的な表記法は、いくつかの並行性と通信の拡張機能とともに、ダイクストラのプログラミングの分野からのものになります。

EWDとは異なり、最終的には生徒に実際の実行可能プログラムを作成してもらいたいと思います。つまり、ある時点でEWD表記から他の言語に翻訳することを意味します。私が最初に正式なプログラミングを始めたとき、私はCをターゲットにしましたが、多くの配管を書くことになります。さらに、ポインターの処理などの複雑さがすべてあります。Rubyは、SchemeやLispと同様に、明らかに可能なターゲットです。しかし、さまざまな機能言語もあります。私は特に並行性に興味があるので、Erlangは可能性のようです。

それで、最後に、私の質問があります：彼らの正式に開発されたプログラムをターゲットにするために、私は私の読者にどの言語を教えるべきですか？

私は情報検索に興味のあるソフトウェア開発者です。現在、私は 3 番目の検索エンジン プロジェクトに取り組んでおり、同じバグなどで何度も何度も書かれているボイラープレート コードの量に非常に不満を感じています。

基本的な検索エンジンは、次の 2 つの「レイヤー」で構成される形式言語で記述できる非常に単純な獣です。

1. 「プリミティブのレイヤー」（または公理、カーネル言語-名前の付け方がわからない）。それらは、いくつかのセット (リソースのセットとして - ファイル、Web サイト)、セット上の関係 (「サイト A がサイト B にリンクする」など)、および「リソース A へのストリームを開く」、「ストリームからレコードを読み取る」などの単純な操作で構成されます。 「N 個のストリームをマージ」、「フィールド F によるレコードのインデックス セット」など。また、「YAML 形式でストリームを保存」、「XML 形式からストリームをロード」など、多くのデータ変換があります。

2. 「アプリケーション層」 - 「新しいリソースの収集」、「収集されたリソースのクロール」、「クロールされたリソースのデータベースへのマージ」、「クロールされたリソースのインデックス作成」、「インデックスのマージ」など、検索エンジンのライフサイクルを形成するいくつかの非常に高レベルの操作など。この高レベルの操作はすべて、1 から「プリミティブ」の用語で表現できます。

このような高レベルの表現は、選択したプログラミング言語で簡単にテストでき、おそらく正式に証明され、実装 (またはコード生成) できます。

では、質問: この方法でシステムを設計する人はいますか? 形式的に、厳密に (おそらく代数/群論のレベルでも)、厳密なトップダウン アプローチで? 何を読めば学べますか?

私はしばらくの間、形式的な方法に興味を持っていました。私は、私が取り組んできたいくつかのプロジェクトのいくつかの非常に具体的なサブエリアについて、形式的な方法を使用して推論しました。正式な方法でドメイン全体を指定するどころか、他のチーム メンバーに同じことを試みるよう説得することはできませんでした。

私が特に興味深いと思った 1 つの方法は、Alloyです。概念的にも表記的にも実際のプログラミング言語に非常に近いため、プロジェクト全体の基盤としてより「スケーリング」できると思います。さらに、ツールは非常に堅牢であるため、モデル検証の利点をすぐに利用できます。

皆さんのプロジェクトで Alloy を使用した実際の経験についてお聞きしたいと思います。より良いドメイン モデルの設計に役立ったと思いますか? 検証中にドメイン モデルにエラーが見つかりましたか? また利用しますか？

大きなテストを小さなテストに分割して、小さなテストが合格したときに大きなテストも合格することを意味するようにしたいと考えています (したがって、元の大きなテストを実行する理由はありません)。小規模なテストは通常​​、時間も労力もかからず、脆弱性も少ないため、これを行いたいと考えています。このテスト分割を堅牢な方法で実現するのに役立つテスト設計パターンまたは検証ツールがあるかどうかを知りたいです。

誰かが小さなテストのセットで何かを変更すると、小さなテストと元のテストの間の接続が失われるのではないかと心配しています。もう 1 つの懸念は、小規模なテストのセットが実際には大規模なテストをカバーしていないことです。

私が目指しているものの例：

私はソフトウェアのモデルの一貫性のチェックに取り組んでいます。これを行うには、UML2.0シーケンス図の線形時相論理を作成する必要があります。体に同じツールが他にある場合は、できるだけ早く対応してください。私はあなたに非常に義務があります。私は魅力的なツールが同じためのプラグインを持っていることを発見しました。魅力的なツール（CHecking ARchitectural ModelconsistentY）のソースコードを持っている人はいますか？彼らのウェブサイトでは利用できません。

前もって感謝します。

正式な側面を使用してコードを作成する場合、ループ不変条件を決定する一般的な方法はありますか、それとも問題によって完全に異なりますか？

私はプログラミングの人生の比較的遅い時期にカリーハワード同形性に出くわしました、そしておそらくこれは私がそれに完全に魅了されることに貢献しています。これは、すべてのプログラミングコンセプトに対して、形式論理に正確な類似物が存在すること、およびその逆が存在することを意味します。これが私の頭のてっぺんからのそのようなアナロジーの「基本的な」リストです：

それで、私の質問に：この同型写像のより興味深い/あいまいな意味のいくつかは何ですか？私は論理学者ではないので、このリストで表面をかじっただけだと確信しています。

たとえば、これは私が論理の中で下品な名前に気付いていないいくつかのプログラミングの概念です：

そして、ここに私がプログラミング用語で完全に特定していないいくつかの論理的な概念があります：

編集：

回答から収集されたいくつかの同等物は次のとおりです。