所以...正規方法和企業
我教軟件工程的形式化方法。我還教「敏捷方法論」。大多數人似乎認爲這是矛盾的。我認爲這很有道理......我也爲一家公司工作，我們需要實際完成工作:)雖然我可以在日常工作中將我的技能點應用於「規範」，但我的同事通常會逃避「正式」這個詞。
我曾經認爲這是由於我們學習如何編程的內在方式：我們通常被驅使找到一個工作解決方案，而不是理解問題。然後我認爲這是由於這樣一個事實，即正式社區中的大多數人不是工程師，而是數學家或計算機科學家。現在，我想知道是否僅僅因爲形式化方法社區隱藏了某種使用UNICODE符號的「混淆」法則，積極開發粗魯的，不合理的工具，並在標準面前大笑。
是的，我已經從一個「怪他們」移動到「怪我們」的角度;-)
所以，我的問題是：你用任何一種形式化方法在你的公司？你有沒有介紹過它們，還是他們的先決條件？你用什麼技術來消除人們恐懼中的數學迷霧，並煽動他們使用形式化的方法？您認爲目前的工具缺乏更廣泛的用途？
讓人們購買任何方法或方法的關鍵是向他們展示它如何解決他們遇到的問題。如果他們能看到這會讓他們的生活更美好，那麼他們有更多的機會讓他們採用這些技術。
如果你不能告訴他們，也許你想採用基於哲學而不是實用性的方法。除非其他人分享你的哲學，否則你不會去任何地方。也許你不應該。
數十年來，已經有很多方法。較新的項目總是解決舊項目的缺點，然而項目仍然陷入困境並失敗。爲什麼？因爲提出新方法的搖滾明星是搖滾明星，並且正是因爲他們理解潛在問題以及如何應用它們而創造出一種新方法。那些後來的人往往盲目地遵循配方，而且效果不好。
因此，我認爲最好的辦法是教導的基本問題，然後展示如何將各種方法試圖解決這些問題。公司，項目和團隊的差異非常大，以至於沒有一種方法可以成功應用於所有組合。學習如何選擇合適的工具並將其應用至關重要。
我參加了「規範和驗證」課程。作爲課程結構的一部分，我們正在做以下工作 - 1.學習工具如PVS（原型驗證系統）http://pvs.csl.sri.com/和SMV（軟件建模和驗證）http://www.cs.cmu.edu/~modelcheck/smv.html 2.除此之外，我們還分析了因軟件故障而發生的事故。對於例如 - 阿麗亞娜V的失敗
我覺得正式方法更適用於失敗成本高於設計成本的情況。它似乎很適合用於關鍵系統中使用的軟件。我想它被用於航空電子設備，芯片設計等，而目前的汽車行業也正在將其付諸實踐。
我試圖讓人們多次接受正式的規範方法（Z和Alloy），並且做出了與您一樣的體驗：大多數人雖然覺得自己有用，但使用起來很不舒服爲實際工作。
有趣的是，同樣的人更樂於生產完全無用的UML圖，數量巨大。
我認爲有這個原因主要有兩個：
一）許多開發人員通過一個正式的方法所需的抽象水平不舒服。大多數入門級數學教育都是微積分和非離散數學都可能需要做些什麼。
b）正式方法需要非常自下而上的設計方法，您可以從頭開始設計核心模型並使其氣密，然後通過在其上提供接口將其連接至實際用戶要求。由於我們傾向於推動開發工作，所以自上而下的方法會更加自然，儘管它往往會導致模型不一致。這就像在房屋已經建成之後在你房子下面改造一個地下室。
如果開發人員不得不每天處理數百萬個設計不佳的抽象，那麼開發人員如何才能對所需的抽象級別感到不舒服？ – 2010-01-22 09:17:58
與企業中的IT業務發展的線路工作意味着必須從實際的商務人士傳授知識有關的業務開始，開發者的頭腦。雖然我自己發現抽象數學是最偉大的逍遙時光之一，但它是一種可怕的通訊工具。通信就是它的全部內容。雖然我可以想象一些成功的說服IT人士接受更抽象的符號，但我基本上沒有商業人士的機會。
儘管在某些領域我可以看到企業中形式化方法的角色（數學和邏輯強大的專業軟件，對於安全關鍵軟件中的可證明屬性的重大需求），但他們幾乎沒有獲得正確要求的幫助在例如如何通過向一組可能的外部或內部供應商發佈一個或多個供應訂單來完成客戶訂單。
我認爲陪審團仍然缺乏基於模型的方法和領域特定語言。我認爲他們會成功還是失敗，取決於他們是否提供IT的快速反饋以滿足業務方面的願望和需求，以及他們是否認爲商業人士將不得不做任何重要的學習。
技術很簡單。溝通很難。正式的方法可能會幫助我們做正確的事情，但是我所見過的方法無助於我們做正確的事情。 （是的，這些都是老生常談，但這是因爲他們是不可避免和痛苦的事實。）
形式化方法使系統沒有任何意義，其中失敗的成本低。
在生產Web應用程序，你有多個前端箱，多個後端盒，多個數據庫箱 - 如果其中任何一個程序出現故障，這是一個非事件。硬件非常便宜，您可以構建這些系統遠遠低於正式指定所有軟件的成本。
謝謝你的貢獻。他們非常有見地。請允許我火焰位（不要把它個人，雖然:-)
大多數人似乎認爲，正規的方法只是對程序驗證。或關鍵系統。如果我們追求最終的陳詞濫調，這可能是事實：證明我們正在做的程序是正確的（v.s.驗證，作爲貢獻者說，如果我們正在做正確的程序，請求）。
但考慮模型查找/檢查工具，如合金。學習如何使用這樣的工具對於習慣於UML和OO的人來說花費的時間可以忽略不計。不過，它可以讓你立即洞悉你的模型。通常需要不到10分鐘的時間才能在模型試圖使用的足夠小的子集上找到反例（包括首先在Alloy中描述模型）。
以需求工程爲例。一個通常會繪製大量的UML。儘管如此，很少有人使用OCL，許多業務規則都以自然語言進行了非正式的註釋。爲什麼？時間限制？
現在考慮一個事實，即大多數人只是用她/他的直覺來證明模型是可以滿足的。同樣，爲什麼？我可以花費相同的時間（可能更少，因爲我不需要關心繪製美學）在Alloy中編寫該模型，只需檢查可滿足性？我現在需要什麼樣的數學？ 「謂詞」？ IFs和布爾值的花式名稱;-)量詞？ ForEachs的花式名稱（）...
大信息系統呢？他們不需要非常關鍵......只需在您的腦海中分析一個包含600多個課程的概念性（而非實施）圖。我看到很多人用容易犯錯的模式犯錯，因爲他們錯過了一些限制，或者模型允許愚蠢的事情發生。
事實是，人們不需要從頭到尾使用正式的方法。當然，我可以在Coq中證明一個完整的應用程序，並證明它是100％符合某些規範。這可能是計算機科學家/數學家的方法。
儘管如此，GTD philisophy爲什麼我不能委託計算機執行一些任務並允許它改善我的開發？這究竟是一個「時間」的問題，還是簡單的，簡單的缺乏技術能力和學習/創新的意願？
大部分工具缺乏的是 - 1.他們不是很直觀。缺乏易於使用的IDE增加了這個原因。 2.需要一些功能編程的知識。我覺得在PVS的情況下，因爲它基於LISP，並且一旦我開始學習Scheme，它就開始具有一定的意義。 – Arnkrishn 2009-03-02 02:02:50