在实际项目中使用 Alloy 的经验

StackOverflow https://stackoverflow.com/questions/2334256

题

我对形式化方法感兴趣已有一段时间了。我使用形式化方法来推理我一直在从事的一些项目的一些非常具体的子领域。我从来没能说服其他团队成员尝试同样的事情，更不用说用正式的方法指定整个域了。

我发现特别有趣的一种方法是 合金. 。我认为它可以更好地“扩展”作为整个项目的基础，因为它在概念上和符号上都非常接近实际的编程语言。此外，这些工具非常可靠，因此可以轻松获得模型验证的好处。

我非常有兴趣了解你们在项目中使用合金的实际经验。您认为它对您设计更好的领域模型有帮助吗？验证过程中是否发现域模型存在错误？你会再次使用它吗？

有帮助吗？

解决方案

是的，我用合金和它的表兄弟工业。合金一直是最有帮助的在说服我，我的模型是不完全错误---或者更确切地说，显示我在哪里，他们都错了，并产生了愚蠢的结果。其他更具体的工具，如宋的雅典娜和格特曼和RAMSDELL的CPSA已在其较窄的领域得到更为有用。你想什么更多的是听到什么？

其他提示

我使用的几个项目和合金发现它有助于;一些但不是全部的我已经能够说服他人参与使用合金为好，或者至少工作与合金模型，我写的项目。这些项目可能是也可能不是你心目中的要求“真实世界”的项目，但他们肯定发生在现实世界中的我工作的一部分。

在2006年和2007年，我创建为当时当前的W3C XPROC规范的草案的部分合金模型;据我所知，该工作组的大多数成员从来没有读过我写的论文（在的 http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html ）;他们说：“哦，我们改变了上周规范的一部分，所以什么模型认为不再相关。”但纸还是设法说服规范，在规范的第一份草案中描述的抽象的“组件”水平远远得以确认，需要进行要么完全指定或丢弃的编辑。他放弃了它，与（我认为）良好的业绩规范的可读性和实用性。

在2010我提出的XPath 1.0中的数据模型的合金模型，发现了一些毛刺在规范。最感兴趣的各方（包括负责维护的XPath 1.0规范的W3C工作组）的反应了，不幸的是，并不令人鼓舞。

一个研究项目我参与使用了合金的MLCD重叠语料库，样本文件的收集和我们正在创造（超链接在SO的坚持抑制）相关信息模型;合金模型中发现一对情侣在我们最初的设计语料库目录错误的，所以这是非常值得的。

和我们也使用了合金形式化我们在转录的性质和类型/令牌的区分文档结构（对我们的报纸，寻找Balisage 2010年诉讼程序的扩展做了一些建模工作：标记会议）。这个谎言合金通常的应用领域之外一点点，因为它无关的软件设计，但合金的检查一致性模型和生成实例的能力是非常宝贵的在向我们展示了一些这样或逻辑后果可能公理我们的模型。

要回答您的具体问题：是的，合金已经帮我清洁指定的域模型，是的，它已经发现的错误和故障。他们往往较小，在他的书的原因丹尼尔·杰克逊解释的软件抽象的：第一，如果你的设计过程中使用的模型，你及早发现错误，当时的所有的仍然是小。而且，第二（在杰克逊的话），“事后看来，大多数的软件设计问题是微不足道的。”

他继续说：“但是，如果你不解决他们硬碰硬，琐碎的问题都成为平凡的一个坏习惯。”我的经验充分证明了这一点。好多早来阻止这样的问题。所以，是的，我将再次使用合金。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top