规范、建模和编程基本上是一样的，对吧？

Question

在基于抽象代数类型和方程理论的形式规范中，您可以使用方程理论的公式来指定理论。在形式逻辑中，满足这些约束的系统称为模型。

建模是创建模型的过程，它抽象了某些方面，这些方面对于特定情况来说是不必要的细节。因此，具体的系统必须在观察到的方面坚持创建模型。

编程是一个创建程序的过程，该程序将具有特定的行为-将执行特定的算法-编程语言通过不同的范例使我们能够以某种特定的方式思考，抽象出一些细节，通常是机器特定的细节。

那么，我们是否可以同时做所有这些事情，因为它们基本上是相同的？声明性编程是不是最近的尝试呢？我们是否可以使用一些编程语言，这些语言对编程、建模和规范都有好处？

Answer 1

在这一观点上做出最大贡献的科学家是托尼·霍尔。Tony和他的同事Edsger Dijkstra一起倡导非确定性编程语言，以便从规范到实现有一个更平滑的路径。Tony肯定想要一种用于规范和实现的单一语言。有关此观点的更多信息，请阅读他的《编程的代数》一书。Tony还在证明抽象的正确性方面做了开创性的工作。所有这些工作都是在简单、命令式语言的上下文中完成的，这些语言具有结构化的控制流和经典的副作用过程。因此，这与必要的声明性编程没有任何联系。从历史上看，函数式编程(声明性编程的主要分支)的工作更多地沿袭了Backus的图灵演讲，主题是“将编程从von Neumann瓶颈中解放出来”；函数式编程与其他编程一样都是关于编程效率的。

自从Hoare以来，我们发现形式规范和形式模型都是非常昂贵的。除非在非常特殊的情况下，例如“如果软件不工作，病人会死”或“如果软件不工作，飞机会坠毁”，否则这笔费用是不合理的。非正式的模型和规范非常有用，而且生产和使用成本要低得多。在建模、模型检查等方面，仍有一些有趣的研究在进行。我个人最喜欢的一种语言是麻省理工学院的Daniel Jackson团队开发的合金语言。微软研究院也做了很好的工作，其他地方也有很多好的工作。声明式编程也有一些工作，但它也是“廉价而愉快”的，而不是像Hoare那样的全面的、程序化的方法。我最喜欢的是Claessen和Hughes的QuickCheck，它提供了一种通过随机测试来声明形式属性和探索它们的方法。没有证明或定理，但仍然非常有用。

总之，您描述了完成正式模型、规范和程序的议程，所有这些都在一个框架内。仍然有很多好的工作在零敲碎打地进行，但是统一的议程已经被抛弃了。