我对形式化方法很感兴趣。我使用形式化方法来推理一些我一直在做的项目中的一些非常具体的子领域。我从未能够说服其他团队成员尝试相同的方法,更不用说使用形式化方法来指定整个领域了。
我发现特别有趣的一种方法是Alloy。我认为它可能更适合作为整个项目的基础,因为它在概念上和符号表达法上非常接近实际的编程语言。此外,工具相当可靠,因此模型验证的好处很容易获得。
如果你们在项目中使用Alloy的实际经验,我会非常感兴趣听听。你们觉得它帮助你们设计更好的领域模型吗?在验证过程中是否发现了领域模型中的错误?你们会再次使用它吗?