11

そう...

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

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

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

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

4

6 に答える 6

3

すべての貢献に感謝します。彼らは非常に洞察力があります。少し炎上させてください（ただし、個人的なことはしないでください:-)

ほとんどの人は、形式的手法はプログラムの検証にすぎないと考えているようです。または重要なシステム。これは、私たちが究極の決まり文句を追求する場合に当てはまるかもしれません: プログラムを正しく行っていることを証明することです (貢献者が言ったように、正しいプログラムを行っているかどうかを尋ねる検証とは異なります)。

ただし、Alloy などのモデル検索/チェック ツールを検討してください。UML や OO に慣れている人にとって、このようなツールの使い方を学ぶのにかかる時間はごくわずかです。それでも、モデルに関する洞察をすぐに得ることができます。通常、使用しようとしているモデルの十分に小さいサブセットで反例を見つけるのに 10 分もかかりません (最初に Alloy でモデルを記述することも含まれます)。

要件エンジニアリングを例に挙げてみましょう。通常、多くの UML を描画します。ただし、OCL を使用する人はほとんどおらず、多くのビジネス ルールには自然言語で非公式に注釈が付けられています。なんで？時間の制約？

ここで、モデルが満足できるものであることを証明するために、大多数が直感を使用するだけであるという事実を考えてみましょう。繰り返しますが、なぜですか？そのモデルを Alloy で記述し、満足できるかどうかをチェックするだけで、同じ時間 (おそらく、描画の美学を気にする必要がないため、さらに短い時間) を費やすことができますか? そして、今、私はどのような数学を必要としていますか? 「述語」？IF とブール値の派手な名前 ;-) 量指定子? ForEachs() の凝った名前...

ビッグ情報システムはどうですか？批判的である必要はありません... 600 を超えるクラスを含む概念図 (実装ではない!) を頭の中で分析してみてください。いくつかの制約を逃したか、モデルがばかげたことが起こるのを許したために、モデルの間違いを犯しやすいことに頭を悩ませている人をたくさん見てきました。

実際、頭から尻尾まで形式的なアプローチを使用する必要はありません。確かに、Coq でアプリケーション全体を証明し、ある仕様に 100% 準拠していることを証明できます。これは、コンピューター科学者/数学者のアプローチかもしれません。

それでも、GTD の哲学があるのに、一部のタスクをコンピューターに委任して、開発の改善に役立てることができないのはなぜでしょうか? それは本当に「時間」の問題なのか、それとも単に技術的能力や学習/革新への意志の単純な欠如なのか?

于 2009-03-06T17:35:41.527 に答える
2

企業内で事業部門の IT 開発に携わるということは、ビジネスに関する知識を実際のビジネス担当者から開発者の責任者に伝達する必要があることを意味します。私自身、抽象的な数学が最高の娯楽の 1 つであることに気づきましたが、それはひどいコミュニケーション ツールです。そして、コミュニケーションこそがすべてです。IT 担当者にもっと抽象的な表記法を採用するよう説得することにはある程度成功するかもしれませんが、基本的にビジネス担当者にはチャンスがありません。

企業内でフォーマルメソッドの役割が見られる領域がいくつかありますが (数学とロジックが重い専門ソフトウェア、安全性が重要なソフトウェアのように証明可能なプロパティが非常に必要とされる)、それらは正しい要件を取得するのにほとんど役に立ちません。可能な外部または内部プロバイダーのセットに 1 つ以上の供給注文を発行することにより、顧客の注文を履行します。

モデルベースのアプローチとドメイン固有言語については、まだ結論が出ていないと思います。ビジネス側の要望やニーズに対して IT からより迅速にフィードバックを提供するかどうか、ビジネス パーソンがかなりの勉強をしなければならないと想定するかどうかによって、成功するか失敗するかが決まると思います。

テクノロジーは簡単です。コミュニケーションが難しい。形式的な方法は、私たちが正しいことをするのに役立つかもしれませんが、私が見たものは、正しいことをするのに何の役にも立たない. （はい、これらは決まり文句ですが、それは避けられず、痛ましいほど真実だからです。）

于 2009-03-05T17:51:02.760 に答える
1

私は人々に形式仕様法（ZとAlloy）を数回受け入れさせようとし、あなたと同じ経験をしました。ほとんどの人は、それらが有用な目的を果たしていると感じながら、実際の作業にそれらを使用することは非常に不快です。

おかしなことに、同じ人々は、まったく役に立たないUML図を大量に作成することに満足しています。

これには2つの主な理由があると思います。

a。）多くの開発者は、正式なアプローチに必要な抽象化のレベルに不快感を覚えています。ほとんどの初級レベルの数学教育がすべて微積分であり、非離散数学であるという事実は、これで何かをしなければならないかもしれません。

b。）形式手法では、コアモデルをゼロから設計して気密にし、その上にインターフェイスを提供して実際のユーザー要件に接続する、非常にボトムアップの設計アプローチが必要です。要件によって開発作業が促進される傾向があるため、モデルの一貫性が失われることがよくありますが、トップダウンアプローチの方が自然に感じられます。それは、家がすでに建てられた後、家の下に地下室を改造するようなものです。

于 2009-03-04T10:00:27.843 に答える
1

形式的な方法は、失敗のコストが低いシステムでは意味がありません。

運用 Web アプリケーションでは、複数のフロントエンド ボックス、複数のバックエンド ボックス、複数のデータベース ボックスがあります。それらのいずれかでプログラムが失敗した場合、それは問題ではありません。ハードウェアは非常に安価であるため、すべてのソフトウェアを正式に指定するコストよりもはるかに少ないコストでこれらのシステムを構築できます。

于 2009-03-05T19:39:07.353 に答える
1

「仕様と検証」のコースを受講しています。コース構造の一環として、次のことを行っています。 1. PVS (プロトタイプ検証システム) http://pvs.csl.sri.com/や SMV (ソフトウェア モデリングと検証) http://www.csなどの学習ツール.cmu.edu/~modelcheck/smv.html 2. それとは別に、ソフトウェアの障害が原因で発生した事故を分析します。例-Ariane Vの失敗

失敗のコストが設計のコストよりも高いシナリオでは、正式な方法の方が適切だと思います。そして、重要なシステムで使用されるソフトウェアにそれらを使用する傾向があるようです。アビオニクスやチップ設計などで使われていると思いますし、現在の自動車業界でも実際に起草されています。

于 2009-03-02T01:56:51.127 に答える