所以...正规方法和企业
我教软件工程的形式化方法。我还教“敏捷方法论”。大多数人似乎认为这是矛盾的。我认为这很有道理......我也为一家公司工作，我们需要实际完成工作:)虽然我可以在日常工作中将我的技能点应用于“规范”，但我的同事通常会逃避“正式”这个词。
我曾经认为这是由于我们学习如何编程的内在方式：我们通常被驱使找到一个工作解决方案，而不是理解问题。然后我认为这是由于这样一个事实，即正式社区中的大多数人不是工程师，而是数学家或计算机科学家。现在，我想知道是否仅仅因为形式化方法社区隐藏了某种使用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