教学程序设计与形式化方法

查理,

这并不是说函数式语言不适合形式化方法——它们非常适合——但其风格与Dijkstra截然不同。首选方法强调计算证明;请参阅理查德·伯德关于解决数独问题的论文(这很难),或理查德·伯德和菲尔·瓦德勒的教科书。

对于并发性,这在很大程度上取决于您相信什么样的并发模型(以及什么样的形式化方法)。John Reppy的并发ML是一个漂亮的消息传递模型。Erlang还有一个很好的干净限制模型。另一方面,使用锁和关键部分进行编程非常困难,在这种情况下,形式化方法可能会带来更多好处。

您的背景研究可能会感兴趣的另外两个附带评论:

• 我见过的唯一一个将Dijkstra的方法应用于实际系统的程序员是Greg Nelson,他在Modula-3中工作。(格雷格和马克·马纳斯共同编写了支架窗口系统。)

• 杰拉德·霍尔兹曼的建模语言 SPIN 它直接基于Dijkstra的保护命令语言,并且还支持并发。它的目的是模型检查,而不是编程,并且有一些特性,但与形式化方法有很强的联系,能够对断言进行模型检查真的很棒。任何对正式方法感兴趣的人都想看看。

Greg Nelson 纸,或其中之一。客户关系管理(CRM)

忽略显而易见的事实你的想法是什么 favorite programming language 答案,我可以看到两个有用的答案:

一方面,您试图向假定为中级程序员的对象演示方法。如果你选择一种语言,并祝福它作为你的书籍语言,你可能会疏远那些出于某种原因而不喜欢这种语言的潜在读者。既然您正在演示方法,那么您就可以在语言中使用恰好能简要说明您的观点的片段。例如,唯一可以用于演示RIIa的语言可能是C++,但是这一语言对于显示如何执行源分析来说很差。Scheme是源代码分析的理想选择,但它并没有为您提供很多选项来探索强类型的优点(和缺点)。使用多种语言。

我是在Lisp和Scheme上长大的,我爱他们两个。我认为它们是从零开始学习的好语言。但是,我不确定有编程经验的人会喜欢这些语言。如果你的书标题中有Scheme,你将不会在亚马逊上获得很多点击率。:)

C#是一种非常容易学习的语言,它具备了快速深入研究并发性等主题所需的所有基础知识。它具有更大的适用性,因为您也可以针对OO和web概念。它也相当流行,你可以让公司为他们的员工书籍付费,这对销售总是有好处的(“做一个优秀的C#程序员”在费用报销单上比“现代Lisp中的并发性”更重要)。

我不能和Ruby说话,所以就我个人而言,我会咬紧牙关,选择C。

老实说,我不能推荐Ruby做这个。当我在我的商业世界中进行日常编程时,我非常喜欢它,当然比C或Java更喜欢它。但是它的语义定义太模糊了,以至于我对它的信任度不及C语言的一半,尽管我可能会花几个小时讨论一个声明,并查阅取代K&的厚得多的白皮书;R、 最后我非常确信,如果我有一个符合标准的编译器(是的,我知道,我是一个梦想家,但在这里和我一起工作),我知道另一面会发生什么。

我也理解Dikjstra与功能的对比;往回走 reading his papers 他处在一个非常紧迫的世界里;我没有资格说他是否真的走错了路。也许我只是被他的写作和他的思想所震撼。但他似乎很高兴,那么使用 Algol 60 ?

我认为Scheme是一个很好的选择,因为它允许人们(以库的形式)以最基本的要素将不同的抽象付诸实践。 也可以很容易地将方案转换为PVS之类的验证系统( http://pvs.csl.sri.com/ )

我认为您自己应该对您的书所使用的语言有一定的经验,或者有人能够熟练地检查您的代码。

就我个人而言,我会使用CommonLisp,因为我对它很熟悉,而且它是实现任何概念的优秀语言。其他选项可能是Erlang、Haskell、Ruby或Python,甚至可能是一些ML方言。我对C家族(包括C#和Java)有偏见,他们似乎对概念的思考停留在较低的层次。