规范、建模和编程基本上是相同的，对吧？
在基于抽象代数类型和方程理论的形式规范中，您使用方程理论的公式来指定理论。满足这些约束的系统在形式逻辑中称为模型。
建模是创建模型的过程，它抽象了一些方面，这些方面对于特定情况来说是不必要的细节。因此，具体系统必须在观察方面遵循所创建的模型。
编程是创建具有特定行为（将执行特定算法）的程序的过程，并且通过不同范式的编程语言使我们能够以某种特定的方式思考，这种方式抽象了一些细节，通常是机器特定的细节。
那么我们是否可以同时做所有这些事情，因为它们基本上是相同的？声明式编程是最接近的尝试吗？我们是否可以使用某种既适合编程又适合建模和规范的编程语言？
In formal specifications based on abstract algebraic types and equational theory you use formulas of equational theory to specify theory. System which will satisfy those constraints is called in formal logic a model.
Modeling is process of creating a model, which abstracts of some aspects, which are unnecessary details for a specific case. So concrete system has to adhere to created model in observed aspects.
Programming is a process of creating a program which will have specific behaviour - will perform specific algorithms - and programming languages through different paradigms enable us to think in a certain specific way, which abstracts of some details, usually machine specific ones.
So could we be doing all those things at the same time, because they are principially the same? Is declarative programming the nearest attempt to do that? Could we use some sort f programming languages which will be good for programming as well as for modeling and specification?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
为推进这一观点做出最大努力的科学家是托尼·霍尔。 Tony 和他的同事 Edsger Dijkstra 提倡非确定性编程语言，以便从规范到实现有一条更顺畅的路径。 Tony 绝对想要一种用于规范和实现的单一语言。有关此观点的更多信息，请阅读他的《编程 Alegbra》一书。托尼还在证明抽象的正确性方面做出了开创性的工作。所有这些工作都是在简单的命令式语言的背景下完成的，具有结构化的控制流和经典的副作用过程。所以与声明式编程没有任何必然联系。从历史上看，函数式编程（声明式编程的主要分支）方面的工作更多地遵循巴科斯关于“将编程从冯·诺依曼瓶颈中解放出来”的图灵讲座；函数式编程与编程生产力和其他方面一样重要。
自霍尔以来我们发现正式的规格和正式的型号非常昂贵。除非在非常特殊的情况下，比如“如果软件不起作用，病人就会死亡”或“如果软件不起作用，飞机就会坠毁”，这笔费用并没有被证明是合理的。非正式的模型和规格非常有用，而且生产和使用的成本要便宜得多。在建模、模型检查等方面仍然有一些有趣的研究正在进行。我个人最喜欢的语言之一是麻省理工学院 Daniel Jackson 团队开发的 Alloy 语言。微软研究院也做出了很多很棒的事情，其他地方也做了很多好事情。在声明性编程方面也有一些工作，但它也是“廉价而愉快”的种类，而不是像霍尔那样全面的编程方法。我最喜欢的一个是 Claessen 和 Hughes 的 QuickCheck，它提供了一种陈述形式属性并通过随机测试探索它们的方法。没有证明或定理，但仍然非常有用。
总之，您描述了在一个框架内执行正式模型、规范和程序的议程。仍然有很多好的工作在零星进行，但统一的议程已被放弃。
The scientist who has done the most to advance this point of view is Tony Hoare. Tony, along with his colleague Edsger Dijkstra, advocated nondeterministic programming languages so that there would be a smoother path from specification to implementation. Tony definitely wanted a single language for both specification and implementation. For more on this view, read his book on the Alegbra of Programming. Tony also did the seminal work on proving correctness of abstractions. All of this work was done in the context of simple, imperative languages with structured control flow and classic, side-effecting procedures. So there is not any connection with declarative programming of necessity. And historically, work on functional programming (the main branch of declarative programming) has followed more from Backus's Turing lecture on "liberating programming from the von Neumann bottleneck"; functional programming has been about programming productivity as much as anything else.
What we discovered since Hoare is that formal specifications and formal modelsl are very expensive. The expense hasn't been shown to be justified except in very special circumstances, like "if the software doesn't work, the patient will die" or "if the software doesn't work, the plane will crash." Informal models and specifications are quite useful, and much cheaper to produce and work with. There is still interesting research going on around the fringes on modelling, model checking, and so on. One of my personal favorites is the Alloy language done by Daniel Jackson's group at MIT. There's also great stuff done at Microsoft Research and plenty of good stuff elsewhere. There's some work in declarative programming as well, but it too is of the "cheap and cheerful" variety rather than a comprehensive, programmatic approach like Hoare's. One of my favorites there is Claessen's and Hughes's QuickCheck, which provides a way to state formal properties and explore them by random testing. No proofs or theorems, but still jolly useful.
In summary, you describe an agenda of doing formal models, specifications, and programs, all within a single framework. There is still plenty of good work going on piecemeal, but the unified agenda has been abandoned.