教学编程和形式方法

这是一个奇怪的问题.我正在编写一本关于学习使用正式方法编程的书,我将把它定位到具有一些编程经验的人.我们的想法是让他们成为高素质的程序员.

基本符号将来自Dijkstra的编程规则,以及一些并发和通信扩展.

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

所以,最后,我的问题是:我应该用什么语言教我的读者定位他们正式开发的程序？

查理,

我一直将Dijkstra的杰作与编程模型联系起来,其中中心阶段由循环和数组占据.如果你坚持靠近Dijkstra(例如,计算最弱的前提条件),我想你会发现函数式语言并不适合.在通过循环和数组进行命令式编程方面提供良好支持的流行语言中,Python可能带来最少的额外包袱.

这并不是说功能语言不适合正式的方法 - 它们非常适合 - 但风格与Dijkstra完全不同.首选方法强调计算证明; 请参阅理查德伯德关于解决数独(这是重要的)或理查德伯德和菲尔沃德勒的教科书的论文.

对于并发性,它很大程度上取决于你所信仰的并发模型(以及正式的方法).John Reppy的Concurrent ML是一个漂亮的消息传递模型.Erlang也有一个很好的清洁限制模型.另一方面,使用锁和关键部分进行编程非常困难,在这种情况下,正式方法可能会带来更多好处.

您可能对您的背景研究感兴趣的另外两个及时的评论:

我见过的唯一一个将Dijkstra的方法应用于实际系统的程序员是Greg Nelson,他在Modula-3工作.(Greg和Mark Manasse一起编写了Trestle窗口系统.)Modula-3是一种非常好的语言,Digital允许他通过无耻和无能而死.格雷格有一篇关于Dijkstra微积分扩展的TOPLAS论文.

Gerard Holzmann的建模语言SPIN直接基于Dijkstra的保护命令语言,它还支持并发.它的目的是模型检查,而不是编程,并且有一些特性,但与正式方法有很强的联系,能够模拟检查断言真的很棒.任何对正式方法感兴趣的人都想查看一下.

(编辑:这是Greg Nelson论文的链接,或者其中之一. - CRM)

忽略你最喜欢的 编程 语言明显的答案,我可以看到两个有用的答案:

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

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