规范、建模和编程原则上是相同的,对吗?

最能推进这一观点的科学家是托尼·霍尔。Tony和他的同事Edsger Dijkstra提倡非确定性编程语言,以便从规范到实现有一个更平滑的路径。托尼肯定想要一个 单一的 用于规范和实现的语言。关于这个观点的更多信息,请阅读他的书 程序设计的阿勒格布拉 . 托尼还做了证明抽象正确性的开创性工作。所有这些工作都是在简单的命令式语言和结构化的控制流以及经典的副作用过程的背景下完成的。因此,与必要的声明性编程没有任何联系。从历史上看,功能编程(声明性编程的主要分支)的工作更多地是从巴科斯的图灵讲座“将编程从冯·诺依曼瓶颈中解放出来”开始的;功能编程和其他任何东西一样,也是关于编程生产力的。

自霍尔以来,我们发现正式规范和正式模型 非常贵 . 除非在非常特殊的情况下,如“如果软件不起作用,病人会死”或“如果软件不起作用,飞机会坠毁”,否则这些费用没有被证明是合理的。非正式的模型和规格是非常有用的,而且生产和使用成本要低得多。在边缘的建模、模型检查等方面仍有一些有趣的研究正在进行。我个人最喜欢的语言之一是麻省理工学院丹尼尔·杰克逊小组的合金语言。微软研究院也做了很多很棒的工作,其他地方也有很多不错的工作。在声明性编程中也有一些工作,但它也具有“廉价和愉快”的多样性,而不是像霍尔那样的全面的、程序化的方法。我最喜欢的是Claessen和Hughes的QuickCheck,它提供了一种陈述形式属性并探索它们的方法。通过随机测试。没有证明或定理,但仍然有用。

总之,你描述了一个做的议程 正式的 模型、规范和程序都在一个框架内。零碎的工作还是有很多不错的,但是 统一的议程已被放弃。