正式方法和企业[关闭]

Question

因此...

我教授软件工程中的正式方法。我还教导了“敏捷方法论”。大多数人似乎认为这是矛盾的。我认为这很有意义......我也为一家公司工作，我们需要实际完成任务:)虽然我可以将我所获得的技能点应用于“规范”。在日常工作中，我的同事们通常会逃避“正式”这个词。

我曾经认为这是由于我们学习如何编程的内在方式：我们通常会找到一个有效的解决方案而不是理解问题。然后我认为这是因为正式社区中的大多数人不是工程师，而是数学家或计算机科学家。如今，我想知道它是否仅仅因为正式方法社区隐藏在某种“混淆”背后。法律使用所有可用的UNICODE符号，积极开发粗鲁，不实用的工具，并在标准面前大笑。

是的，我一直在改变“责备他们”。对“责怪我们”观点; - ）

所以，我的问题是：你在公司使用任何形式的方法吗？你介绍过它们，还是它们的先决条件？你用什么技巧来消除人们的恐惧中的数学迷雾，并煽动他们使用正式的方法？您认为目前的工具缺乏更普遍的用途？

Answer 1

让人们购买任何方法或方法的关键是向他们展示如何解决他们遇到的问题。如果他们能够看到它会让他们的生活更美好，那么他们有更大的机会让他们采用这些技术。

如果你不能向他们展示，也许你想采用基于哲学而非实用性的方法。除非其他人分享你的哲学，否则你不会去任何地方。也许你不应该这样做。

几十年来，有许多方法论。较新的那些总能解决旧的缺点，但项目仍然遇到麻烦而失败。为什么？因为提出新方法的摇滚明星是摇滚明星，并且已经制定了一种新的方法，因为他们了解潜在的问题以及如何应用它们。那些追求的人往往盲目地遵循食谱，而且效果不好。

所以我认为最好的方法是教导潜在的问题，然后展示各种方法如何尝试处理这些问题。公司，项目和团队的差异如此之大，以至于没有一种方法可以成功应用于所有组合。学会选择合适的工具并将其应用得很好是至关重要的。

Answer 2

感谢您的所有贡献。他们非常有见地。请允许我点火一点（不要把它当作个人，但是： - ）

大多数人似乎认为正式方法只是程序验证。或关键系统。如果我们追求最终的陈词滥调，这可能是真的：证明我们正在正确地执行程序（v.s.验证，作为贡献者，如果我们正在做正确的程序，则要求）。

但考虑模型查找/检查工具，例如Alloy。学习使用这样的工具对于习惯于UML和OO的人来说花费的时间可以忽略不计。不过，它可以让您立即了解您的模型。通常需要不超过10分钟才能找到一个试图使用的模型的足够小的子集的反例（并且包括首先在Alloy中描述模型）。

以需求工程为例。人们通常会画很多UML。但是，很少有人使用OCL，许多商业规则都是用自然语言非正式地注释的。为什么？时间限制？

现在考虑这样一个事实，即大多数人只是用她/他的直觉来证明一个模型是可以满足的。再次，为什么？我可以花费相同的时间（可能更少，因为我不需要关心绘制美学）在Alloy中编写该模型，并检查是否可满足？我现在需要什么样的数学？ ＆QUOT;谓词＆QUOT ;? IF和布尔的花式名称;-)量词？ ForEachs（）的花哨名称......

大型信息系统怎么样？它们不需要是关键的...只是尝试在头脑中分析超过600个类的概念（不是实现！）图。我看到很多人因为错过了一些约束而错过了一些约束，或模型允许愚蠢的事情发生，因此很容易在墙上撞到他们的头。

事实是，人们不需要从头到尾使用正式的方法。当然，我可以在Coq中证明一个完整的应用程序，并证明它100％符合某些规范。这可能是计算机科学家/数学家的方法。

然而，对于GTD哲学家，为什么我不能为计算机委派一些任务并允许它帮助改进我的开发？这真的是“时间”问题，还是简单，缺乏技术能力以及学习/创新的意愿？

Answer 3

在企业中使用业务线IT开发意味着必须将业务知识从实际业务人员转移到开发人员的头脑中。虽然我自己发现抽象数学是最大的逍遥时光之一，但它是一种糟糕的通讯工具。沟通就是它的全部。虽然我可能有一些成功说服IT人员接受更抽象的符号，但我基本上没有机会与商界人士合作。

虽然在某些方面我可以看到企业中正式方法的作用（数学和逻辑繁重的专业软件，对安全关键软件中可证明属性的重大需求），但它们对于获得正确的要求几乎没有帮助例如如何通过向一组可能的外部或内部提供商发出一个或多个供应订单来履行客户订单。

我认为陪审团仍然是基于模型的方法和领域特定的语言。我认为他们会成功还是失败取决于他们是否能够从IT部门提供更快的反馈意见，以及业务方面的愿望和需求，以及他们是否认为商业人士必须进行任何重要的学习。

技术很简单。沟通很难。正式方法可以帮助我们做正确的事情，但我见过的那些方法无助于我们做正确的事情。 （是的，这些都是陈词滥调，但这是因为它们是不可避免和痛苦的。）

Answer 4

我正在学习'规范与验证'课程。作为课程结构的一部分，我们正在做以下事项 - 1. PVS（原型验证系统）等学习工具 http://pvs.csl.sri.com/和SMV（软件建模和验证） http：//www.cs.cmu埃杜/〜的ModelCHECK / smv.html 除此之外，我们还解决因软件故障而发生的事故。对于例如 - 阿丽亚娜V的失败

我认为正式方法更适用于故障成本高于设计成本的情况。并且似乎很容易将它们用于关键系统中使用的软件。我想它用于航空电子设备，芯片设计等，目前的汽车工业也正在起草实践。

Answer 5

我试图让人们多次接受正式的规范方法（Z和Alloy），并且已经达到了相同的目的：大多数人虽然觉得它们有用的目的，却非常不舒服地使用它们实际工作。

有趣的是，同样的人非常乐意以巨大的数量生成完全没用的UML图。

我认为这有两个主要原因：

a。）许多开发人员对正式方法所需的抽象级别感到不舒服。大多数入门级数学教育都是微积分和非离散数学这一事实可能需要对此做些什么。

b。）正式方法需要一个非常自下而上的设计方法，您可以从头开始设计核心模型并使其气密，然后通过在其顶部提供接口将其连接到实际用户要求。由于我们倾向于需要推动开发工作，因此自上而下的方法感觉更自然，尽管它通常会导致模型不一致。这就像在房子建成之后对房屋下面的地下室进行改造一样。

Answer 6

在故障成本较低的系统中，正式方法毫无意义。

在生产Web应用程序中，您有多个前端盒，多个后端盒，多个数据库盒 - 如果其中任何一个上的程序出现故障，那么这是一个非事件。硬件非常便宜，您可以以远低于正式指定所有软件的成本来构建这些系统。