教授编程和形式化方法

Question

教授编程和形式化方法

programming-languagesdijkstraformal-methods

22

这是一个有点奇怪的问题。我正在撰写一本关于使用形式化方法学习编程的书籍，目标读者是有一定编程经验的人。我的想法是教他们成为高质量的程序员。

基本符号将来自Dijkstra的Discipline of Programming，还包括一些并发和通信扩展。

与EWD不同，我希望我的学生最终能够编写实际可执行的程序。这意味着在某个时候需要从EWD符号转换到其他语言。当我开始进行形式化编程时，我将目标指向了C，但你最终会写很多管道代码，加上处理指针等复杂性。Ruby是一个明显的可能目标，Scheme或Lisp也是如此。但也有各种函数语言；由于我特别关注并发，Erlang似乎是一个可能的选择。

因此，最后，我的问题是：我应该教我的读者使用哪种语言来针对他们开发的正式程序？

- Charlie Martin

1

听起来像是一本非常有趣的书！ - Uri

谢谢，我会上传章节供评论，可能会链接到chasrmartin.com。当我有章节时。 - Charlie Martin

2

祝你的书一切顺利，马蒂。我刚刚搜索并找到了“形式化方法”的含义。 - Alphaneo

7个回答

7

忽略显而易见的问题，你最喜欢的编程语言是什么，我可以看到两个有用的答案：

一方面，你试图向被认为是中级程序员的人展示方法。如果你选择一种语言，并将其作为书籍的语言，那么你可能会排斥不喜欢该语言的潜在读者，因为某种原因。由于你正在展示方法，你可以使用能够简洁地说明你的观点的语言片段。例如，用于演示RIIA的唯一可用语言可能是C++，但是这种语言对于展示如何执行源代码分析非常差。Scheme非常适合源代码分析，但是它没有提供很多探索强类型优缺点的选项。使用多种语言。

另一方面，由于你主要关注编程方法，我不确定你是否真正需要任何实际的语言。一个定义良好的符号表示法同样好，并迫使读者关注你所要表达的重点，而不是某种语言的表面细节。

- SingleNegationElimination

1

是的，那是EWD的论点。我不确定我是否同意 -- 我认为使用真正的语言可以让你保持诚实。我还考虑过设计一种Ruby DSL作为教学语言。 - Charlie Martin

你可以使用真实的编程语言，或者多种真实的编程语言，每一种都经过精心挑选，以便在最大程度上展示其说明能力。 - SingleNegationElimination

采用EWD的想法，使用您自己定义的语言。所有真正可执行的语言都有设计缺陷和边缘情况，这使它们变得痛苦。最好拥有一种您可以逐步执行并确信其执行的符号/语言。 - user9903

3

我成长于Lisp和Scheme，非常喜欢它们。我认为它们是从零开始学习的好语言。但是，我不确定有编程经验的人是否会喜欢这些语言。你不会在亚马逊上找到以Scheme为标题的书籍。

C#是一种非常易学的语言，拥有所有您需要快速深入并发等主题所需的基础知识。它具有更广泛的适用性，因为您可以针对面向对象和Web概念进行目标设置。它也相当受欢迎，您将得到公司支付员工图书费用的好处，这对销售始终是有利的（“成为一名出色的C#程序员”比“现代Lisp中的并发”更好）。

F#是一种有趣的语言。它具有Lisp或Scheme的功能美感（虽然不完全如此，但几乎如此），并且还为您提供了一些深入研究面向对象编程主题以及连接到.NET框架进行UI设计的能力。但是，现在它还很鲜为人知。

我不能评论Ruby，所以个人而言，我会选择C#。

- JP Alioto

我只是在等待这个的提示音 :) - JP Alioto

1

好的，我为你投了一票，这是一个完全合理的论点。我怀疑人们在“形式化方法”引起注意之前会逃之夭夭，而“scheme”却未必。我对Win... Win...那个其他操作系统有点偏见，但确实有很多人在使用它。 - Charlie Martin

如果是这种问题，你可以轻松地用Java替换C#。:) 我不确定形式化方法会吓走任何人...当然不会吓走我。即使你从未阅读过它，只是通过渗透作用获得了它的好处，它在书架上看起来也很好。 - JP Alioto

说到并发，形式方法如何处理呢？Dijkstra在这方面的重要性被认识到之前就已经写过了。 - David Thornley

2

说实话，我不建议使用Ruby来做这件事。在我的商业世界中，我每天都会用它编程，我非常喜欢它，当然比C或Java好得多。但它的语义是如此模糊，以至于我不像在C中那样信任它，尽管我可能花费几个小时争论一个语句并参考那本更厚的白皮书（取代了K&R），但最终我还是相当确信，如果我有一个符合规范的编译器（是的，我知道，我是个梦想家，但请和我一起工作），我知道结果是什么。

Ruby在很多方面都很棒，但就正式的东西而言，两者永远无法相遇。

我倾向于投票给Haskell，因为每次我转身时，我都惊讶于这种语言定义的意义有多大。（尽管承认只学了一年左右，我肯定没有探索过Haskell 98的一半角落。）

我也理解Dikjstra与函数式的问题；回头阅读他的论文，他非常处于命令式世界中；我不太确定他是否真的走错了路。也许我只是被他的写作和思想感到不知所措。但这似乎让他感到高兴，那么使用Algol 60怎么样？

- cjs

1

有相当多的大学使用完美开发者来教授正式方法（免责声明：我与此产品有关）。它基于一种用于表达规范、数据细化和算法的语言构建。它有一个自动定理证明器用于验证，以及一个可以生成C++、C#和Java代码的代码生成器。PD的设计受到《编程纪律》的启发，但我们发现该符号对于大型系统而言实际上不太实用，因此该符号在某种程度上已经偏离了迪科斯彻的思路。

- dc42

好的，看起来很有趣。我需要更深入地了解这个，但是我感谢你的指引。 - Charlie Martin

1

这是一个不错的想法。我认为Scheme是一个很好的选择，因为它允许人们使用最少的基本要素来实践（以库的形式）不同的抽象。而且，从Scheme到验证系统（如PVS）的转换也很容易（http://pvs.csl.sri.com/）。

干杯

- Arnkrishn

是的。我非常有兴趣将模型检查引入到这些东西中，但我认为那将是第二本书。我试图推动这个想法，即你可以在不需要证明检查器的情况下学会严谨地思考和编程。 - Charlie Martin

1

我认为你应该在编写书籍时使用自己熟悉的语言，或者请一位熟练的人来审查你的代码。

个人而言，我会使用Common Lisp，因为我熟悉它，并且它是实现任何概念的优秀语言。其他选项可能包括Erlang、Haskell、Ruby或Python，甚至一些ML方言。我对C系列（包括C#和Java）持有偏见，它们似乎停留在更低层次的概念思考上。

- Svante

我对此真的很犹豫。我在我提到的任何选项中都感到相当舒适，所以这不是问题，而且说实话，经过40年的编程，它们看起来都差不多了。你关于C / Java的观点是正确的，但这就是为什么我分两步走：首先编写EWD代码，然后将其翻译为目标语言。 - Charlie Martin

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Norman Ramsey · Accepted Answer

Charlie,

我一直将Dijkstra的杰作与循环和数组占据主要地位的编程模型联系在一起。如果你紧密遵循Dijkstra（例如计算最弱前提条件），我认为你会发现函数式语言不太适合。在流行的提供了循环和数组命令式编程良好支持的语言中，也许Python携带的附加负担最少。

这并不是说函数式语言不适用于形式方法，它们非常适用，但风格与Dijkstra有很大不同。首选的方法强调计算证明; 可以参考Richard Bird关于解决数独的论文（很难懂）或Richard Bird和Phil Wadler的教科书。

对于并发性，这取决于您信仰哪种并发模型（以及哪些形式方法）。John Reppy的并发ML是一种美丽的消息传递模型。 Erlang也具有很好的干净限制性模型。另一方面，使用锁定和关键部分进行编程非常困难，在那种情况下可能更有益于形式方法。

还有两个简短的备注可能对您的背景研究有所帮助：

我曾经遇到的唯一一个将Dijkstra的方法实际应用于真实系统的程序员是Greg Nelson，他正在使用Modula-3进行工作。（Greg和Mark Manasse共同编写了Trestle窗口系统。） Modula-3是一种非常好的语言，数字公司通过无能和无能力而让其消亡。 Greg在Dijkstra演算法的扩展上有一篇不错的TOPLAS论文。
Gerard Holzmann的建模语言SPIN直接基于Dijkstra的保护命令语言，并支持并发性。它的目的是模型检查，而不是编程，有一些特殊之处，但与形式方法存在强烈联系，能够模型检查您的断言真是太棒了。任何对形式方法感兴趣的人都会想看看它。

（编辑说明：这是Greg Nelson的论文链接，或其中一个。— CRM）