正式な方法と企業

Question

だから...

私はソフトウェア工学で正式な方法を教えています。私は「アジャイル方法論」も教えています。ほとんどの人はこれが矛盾していると思っているようです。私はそれがかなり意味があると思う...私は実際に物事を完了する必要がある会社のために働く:)私は日々の基準で "仕様"に私の獲得したスキルポイントを適用することができますが、私は同僚は典型的には「フォーマル」という言葉から逃げる。

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

はい、私は「私たちを責める」の視点;-)だから、

に「彼らを責める」から移動してきた、私の質問です：あなたがあなたの会社に形式手法のいずれかの種類を使用していますか？あなたはそれらを導入しましたか、それとも前提条件ですか？人々の恐怖から数学の霧を解き、正式な方法を使うよう促すためにどのようなテクニックを使いますか？もっと一般的な使い方のために現在のツールには欠けていると思いますか？

Answer 1

の方法や方法論を購入する鍵となるのは、それがどのように問題を解決しているかを示すことです。彼らが自分の人生をより良くすることがわかるなら、彼らに技術を採用させる機会がはるかに増えます。

にはが表示されない場合は、おそらく実用的ではなく哲学に基づく方法を採用したかったでしょう。他の人たちがあなたの哲学を分かち合わない限り、あなたはどこにも行かないでしょう。そしておそらくあなたはしてはいけません。

数十年にわたり、多くの方法論がありました。新しいものは常に古いものの欠点に対処しますが、プロジェクトはまだ問題を起こして失敗します。どうして？新しい方法論を思い付くロックスターはロックスターであり、根本的な問題とそれをどのように適用するのかを理解しているため、新しい方法論を正確に作成しているからです。後に来る者は、盲目的にレシピに従う傾向があり、うまく機能しません。

私は、根本的な問題について教え、それらの問題に対処するためにさまざまな方法がどのように試みられるかを示すことが最善の策だと思います。企業、プロジェクト、チームの違いは非常に大きいので、どの方法もすべての組み合わせにうまく適用できません。適切なツールを選択してそれをうまく適用することを学ぶことが重要です。

Answer 2

私は '仕様と検証'のコースを受講しています。コースの構造の一部として、我々は別に、我々は理由ソフトウェア障害の起きた事故を分析行うことから、PVS（プロトタイプ検証システム）http://pvs.csl.sri.com/とSMV（ソフトウェアのモデリングと検証）http://www.cs.cmu.edu/~modelcheck/smv.html 2のようなfollowing- 1.学習ツールを行っています。例えば、 - Arianeの失敗V

故障コストが設計コストを上回るシナリオでは、正式な方法がより適用可能であると感じます。そして、クリティカルなシステムで使用されているソフトウェアのためにそれらを使用するのが適切と思われます。私はそれが航空電子工学、チップ設計などに使われていると思うし、現在の自動車産業も実際にそれを起草している。

Answer 3

私は人々に正式な仕様方法を数回（Zと合金）取り入れようとしていて、同じexpirienceを持っていました。ほとんどの人は、彼らが有用な目的に役立っていると感じながらも、実際の作業のために。

面白いことに、同じ人たちは、まったく役に立たないUMLダイアグラムを膨大な量で作成することに満足しています。

私は、このために2つの主な理由があると思う：。

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

b。）正式な方法では、コアモデルを初めから設計し、気密にして、上にインターフェイスを提供して実際のユーザー要件に接続する、非常にボトムアップな設計が必要です。我々は、開発努力を推進する要件がある傾向があるので、トップダウンアプローチは、しばしば一貫性のないモデルにつながるが、より自然なものと感じる。それは既に建設された後、あなたの家の下に地下室を改装するようなものです。

Answer 4

企業でのIT開発の作業は、ビジネスに関する知識を実際のビジネス担当者から開発者の責任者に移すことを意味します。私は自分自身で抽象的な数学が最大の娯楽の一つであると考えていますが、それはひどいコミュニケーションツールです。そして、コミュニケーションはすべてそれについてです。私はIT人により抽象的な表記法を受け入れることを確信させるいくつかの成功を見込んでいるかもしれませんが、基本的にビジネスの人たちにはチャンスがありません。

エンタープライズ内で正式なメソッドの役割を見ることができる分野がいくつかありますが（安全上重要なソフトウェアのような証明可能なプロパティの重要なニーズ）、正しい要件の取得にはほとんど役立ちません例えば可能な外部または内部のプロバイダーのセットに1つまたは複数のサプライオーダーを発行することによって顧客の注文をどのように達成するか。

私は陪審員がモデルベースのアプローチとドメイン固有の言語でまだ出ていると思います。私は、彼らがITからビジネス側の要望やニーズに素早くフィードバックするかどうか、そしてビジネスの人々が重要な勉強をしなくてはならないかどうかによって、成功するか失敗するかと思います。

技術は簡単です。コミュニケーションは難しい。正式な方法は正しいことをするのに役立つかもしれませんが、私が見たことは正しいことをするのに役立つものではありません。 （はい、これらは面倒ですが、それは不可避的かつ辛いことですから）

Answer 5

正式な方法は、障害のコストが低いシステムでは意味がありません。

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

Answer 6

ありがとうございます。彼らは非常に洞察力があります。私に少し気を付けてください（個人的ではありません:-)

ほとんどの人は正式な方法はプログラムの検証に関するものだと思っています。または重要なシステム。これは、最終的な決まりを追求している場合には真実かもしれません。プログラムを正しく実行していることを証明することです（v.S.検証、貢献者が言っているとおり、適切なプログラムを行っているかどうかを確認します）。

しかし、合金などのモデル検索/検査ツールを検討してください。このようなツールを使うことを学ぶことは、UMLやOOに慣れた人にとっては無視できるほどの時間がかかります。それでも、それはあなたのモデルを直ちに理解することができます。使用しようとしているモデルの十分に小さいサブセット（そして最初に合金のモデルを記述することを含む）に対して反例を見つけるのに通常は10分以上かかりません。

例として、エンジニアリングを行います。通常、多くのUMLを描画します。 OCLを使用する人はほとんどいません。多くのビジネスルールは、自然言語で非公式に記されています。どうして？時間の制約？

ここで、過半数は、モデルが充足可能であることを証明するために彼女/彼の嫌悪感を使用するという事実を考えてみましょう。もう一度、なぜですか？私は、合金にそのモデルを書くために、同じ量の時間を取ることができます（おそらく、私は美しさを描くことに気を使う必要がないので、さらに少なくて済みます）。そして、私は今どのような数学を必要としていますか？ "述語"？ IFとブール値の素晴らしい名前;-)数量化？ ForEachs（）の名字...

大きな情報システムはどうですか？彼らは批判的である必要はありません... 600以上のクラスを持つ概念的な（実装ではありません）ダイアグラムをあなたの頭で分析しようとします。彼らはいくつかの制約を逃したので、簡単にモデルの間違いをして壁に頭をぶつけている人が多くいます。あるいは、モデルによって愚かなことが起こることがあります。

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

まだ、GTDの教科書では、コンピュータのタスクを委任して開発を改善することができないのはなぜですか？それは本当に「時間」の問題か、あるいは技術的な能力の単純で単純な欠如であり、学ぶか/滅ぼす意志でしょうか？