教授编程和形式化方法

Question

这是一个奇怪的问题。我正在写一本关于学习使用形式化方法进行编程的书，并且我将把它的目标读者定位为具有一定编程经验的人。这个想法是教他们成为高素质的程序员。

基本符号来自 Dijkstra 编程纪律, ，以及一些并发和通信扩展。

与 EWD 不同，我希望我的学生最终能够编写实际的可执行程序。这意味着在某些时候要从 EWD 表示法转换为其他语言。当我第一次开始进行正式编程时，我的目标是 C，但最终你会编写大量管道，而且处理指针等也很复杂。Ruby 显然是一个可能的目标，Scheme 或 Lisp 也是如此。但也有各种函数语言；因为我对并发特别感兴趣，所以 Erlang 似乎是一种可能性。

所以，最后，这是我的问题：我应该教我的读者哪种语言来瞄准他们正式开发的程序？

Answer 1

查理，

我总是将 Dijkstra 的杰作与循环和数组占据中心舞台的编程模型联系起来。如果您坚持使用 Dijkstra（例如，计算最弱的先决条件），我认为您会发现函数式语言不太适合。在为循环和数组的命令式编程提供良好支持的流行语言中，Python 可能是负担最少的。

这并不是说函数式语言不适合形式化方法——它们非常适合——但其风格与 Dijkstra 有很大不同。首选方法强调计算证明；请参阅理查德·伯德（Richard Bird）关于解决数独（难度很大）的论文或理查德·伯德（Richard Bird）和菲尔·瓦德勒（Phil Wadler）的教科书。

对于并发性，它在很大程度上取决于您相信什么并发模型（以及什么形式方法）。John Reppy 的并发机器学习是一个漂亮的消息传递模型。Erlang 还有一个很好的干净的限制模型。另一方面，使用锁和临界区进行编程非常困难，在这种情况下，形式化方法可能会有更多好处。

另外两句话可能对您的背景研究感兴趣：

• 我见过的唯一一位将 Dijkstra 的方法应用于实际系统的程序员是 Greg Nelson，他在 Modula-3 工作。（Greg和Mark Manasse一起编写了Trestle Window系统。）Modula-3是一种非常好的语言，数字可以通过无情和无能死亡。Greg 有一篇关于 Dijkstra 微积分扩展的很好的 TOPLAS 论文。

• Gerard Holzmann 的建模语言 旋转 直接基于 Dijkstra 的受保护命令语言，并且它还支持并发。它的目的是模型检查，而不是编程，并且有一些特质，但与形式方法有很强的联系，能够对你的断言进行模型检查真的很棒。任何对正式方法感兴趣的人都会想检查一下。

（编辑：这是一个链接 格雷格·纳尔逊 纸，或其中之一。— 客户关系管理）

Answer 2

忽略显而易见的收藏 < a href =“https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better”>编程 语言答案，我可以看到两个有用的答案：

一方面，您正在尝试演示假定为中级程序员的方法。如果您选择一种语言并将其作为您的书籍语言加以保护，您可能会疏远那些因某种原因而不喜欢该语言的潜在读者。由于您正在演示方法，因此您可以轻松地使用恰好说明您的观点的语言中的代码段。例如，可用于演示RIIA的唯一语言可能是C ++，但是这种语言在展示如何执行源分析方面相当差。 Scheme是源分析的理想选择，但是没有为您提供很多选项来探索强类型的好处（和弱点）。使用多种语言。

另一方面，由于你主要是编程方法，我不完全确定你需要任何真正的语言。一个定义明确的符号同样好，并且强迫您的读者专注于您正在制作的点，而不是一种语言或其他语言的表面细节。

Answer 3

我在Lisp和Scheme上长大并且非常喜欢他们。我认为它们是从头开始学习的优秀语言。但是，我不确定有某些编程经验的人会采用这些语言。在标题中使用Scheme，你不会在亚马逊上获得大量的点击。 ：）

C＃是一门非常容易学习的语言，它具有您需要的所有基础知识，可以很快地深入了解并发等主题。它具有更多适用性，因为您也可以定位OO和Web概念。它也相当受欢迎，你会让公司为他们的员工支付总是有利于销售的书籍（“Be a Kick Ass C＃Programmer”在费用报销表上远远超过“现代Lisp中的并发”）。

F＃是一种有趣的语言。它具有Lisp或Scheme的功能之美（不是很好，但差不多），并且它为您提供了一些潜入OOP主题的能力，以及如果您想要提高性能，还可以使用.NET框架来获取UI内容。但是，现在，这是模糊不清的。

我不能和Ruby说话，所以我个人会咬紧牙关和C＃一起去。

Answer 4

老实说，我不能推荐Ruby。当我在商业世界中日常编程时，我非常喜欢它，当然比C或Java更多。但它的语义是如此不明确，以至于我不相信C的一半，尽管我可能花了几个小时争论一个声明，并咨询更厚的白皮书取代K＆amp; R，我出来了最后我相信如果我有一个符合规范的编译器（是的，我知道，我是一个梦想家，但在这里和我一起工作）我知道另一方面会发生什么。

Ruby在许多方面都很精彩，但就任何形式而言，twain永远不会满足。

我倾向于亲自投票支持Haskell，因为每次我转身时，我都惊讶于语言定义中所有内容的含义。 （虽然只有一年左右的时间，但我确信我甚至没有探索过Haskell 98的一半角落。）

我也理解Dikjstra与功能性的东西;回去并阅读他的论文他非常关注一个势在必行的世界;我没资格说他是否真的走错了路。也许我对他的写作有多么不满，就像他的想法一样。但它确实让他高兴，那么如何使用 Algol 60 的？

Answer 5

这是一个好主意。 我认为Scheme是一个很好的选择，因为它允许一个人实现（以库的形式）不同的抽象与最基本的必需品。 从方案转换到PVS等验证系统也很容易（ http：//pvs.csl.sri。 COM / ）

欢呼声

Answer 6

我认为你应该对自己用于本书的语言或者熟练检查代码的人有一定的经验。

就个人而言，我会使用Common Lisp，因为我对此很熟悉，而且它是实现任何概念的好语言。其他选项可能是Erlang，Haskell，Ruby或Python，甚至可能是一些ML方言。我对C系列（包括C＃和Java）有偏见，他们似乎坚持对概念的低级思考。

Answer 7

有不少大学使用Perfect Developer来教授正式方法（免责声明：我与此产品有关）。它围绕用于表达规范，数据细化和算法的语言构建。它有一个用于验证的自动定理证明器，以及一个可以生成C ++，C＃和Java的代码生成器。 PD的设计很大程度上受到“A Programming of Programming”的启发，但是我们发现这个符号对于大型系统来说相当不实用，所以这个符号与Dijktra有点不同。