罗伯特·W·弗洛伊德(Robert W Floyd,1936年6月8日-2001年9月25日)是一个知名的计算机科学家,1978年图灵奖得主。
弗洛伊德出生在美国纽约,14岁即完成高中学业,当他1953年从芝加哥大学获得文学学士学位时,年仅17岁,并于1958年在物理学获得了第二个学士学位。
他在1960年代早期成为计算机操作员,并发表了许多出名的论文,并当他27岁时,被任命为卡内基梅隆大学的副教授,并于6年后成为斯坦福大学的正教授。此时他并没有博士学位。
弗洛伊德的主要贡献包括弗洛伊德算法,能有效地发现图的所有最短路径;他的工作有词法解析;他在一篇独立发表的文章里引入了一个重要的概念——图像渲染的误差扩散法,也被称为弗洛伊德-斯坦伯格抖动(但他区分了抖动和扩散)。
他一个显著的成就是开创性地在程序验证中使用了逻辑断言。在他1967年的论文《如何确定程序的意义》Assigning Meanings to Programs中首先提出,之后演化为霍尔逻辑。
弗洛伊德与高德纳工作很密切,他是高德纳的著作《计算机程序设计艺术》的主要评审,并且在书中被多次提及。他与理查德·贝尔格(Richard Beigel)合著有《机器的语言:可计算和形式语言的介绍》The Language of Machines: an Introduction to Computability and Formal Languages。
弗洛伊德于1978年获得图灵奖,并做“程序设计的风范”(The Paradigms of Programming)的演讲,图灵奖引文是: 在构造高效、可靠性软件方法学领域的显著影响;在下列计算机科学重要分支的奠基性的贡献:分析理论,编程语言语义,自动程序验证,自动程序综合生成和算法分析。
罗伯特·弗洛伊德——前后断言法的创始人编辑本段回目录
历届图灵奖得主基本上都有高学历、高学位,绝大多数有博士头衔。这是可以理解的,因为创新型人才需要有很好的文化素养,丰富的知识底蕴,因而必须接受良好的教育。但事情总有例外,1978年图灵奖获得者、斯坦福大学计算机科学系教授罗伯特·弗洛伊德(Robert W.Floyd)就是一位“自学成才的计算机科学家”(a Self-Taught Computer Scientist)。
弗洛伊德1936年6月8日生于纽约。说他“自学成才”并不是说他没有接受过高等教育,他是芝加哥大学的毕业生,但学的不是数学或电气工程等与计算机密切相关的专业,而是文学,1953年获得文学士学位。20世纪50年代初期美国经济不太景气,找工作比较困难,因学习文学而没有任何专门技能的弗洛伊德在就业上遇到很大麻烦,无奈之中到西屋电气公司当了二名计算机操作员,在IBM650机房值夜班。我们知道,早期的计算机都是以批处理方式工作的,计算机操作员的任务就是把程序员编写好的程序在卡片穿孔机(这是脱机的辅助外部设备)上穿成卡片,然后把卡片叠放在读卡机上输入计算机,以便运行程序。因此,操作员的工作比较简单,同打字员类似,不需要懂计算机,也不需要懂程序设计。但弗洛伊德毕竟是一个受过高等教育的人,又是一个有心人,干了一段操作员,很快对计算机产生了兴趣,决心弄懂它,掌握它,于是他借了有关书籍资料在值班空闲时间刻苦学习钻研,有问题就虚心向程序员请教。白天不值班,他又回母校去听讲有关课程。这样,他不但在1958年又获得了理科学士学位,而且逐渐从计算机的门外汉变成计算机的行家里手。1956年他离开西屋电气公司,到芝加哥的装甲研究基金会(Armour Research Foundation),开始还是当操作员,后来就当了程序员。1962年他被马萨诸塞州的Computer Associates公司聘为分析员。1965年他应聘成为卡内基—梅隆大学的副教授,3年后转至斯坦福大学,1970年被聘任为教授。之所以能这样快地步步高升,关键就在于弗洛伊德通过勤奋学习和深入研究,在计算机科学的诸多领域:算法,程序设计语言的逻辑和语义,自动程序综合,自动程序验证,编译器的理论和实现等方面都作出创造性的贡献。其中包括:1962年,弗洛伊德完成了Algol 60编译器的开发,成功投入使用,这是世界上最早的Algol 60编译器之一,而且弗洛伊德在这个编译器的开发中率先融入了优化的思想,使编译所生成的目标代码占用空间少,运行时间短。弗洛伊德优化编译的思想对编译器技术的发展产生了深刻的影响。随后,他又对语法分析进行了系统研究,大家现在熟知的优先文法(precedence grammar),限界上下文文法(bounded context grammar)等都是弗洛伊德在这个时期首先提出来的。优先文法解决了自底向上的语法分析中的首要任务:如何找到“句柄”,也就是当前需要进行归约的符号串。弗洛伊德通过对不同的符号定义不同的优先级,解决了这个问题。限界上下文文法则通过对上下文无关文法G中的两个推导:
*
S→βArβαγ
+
S→δαε
进行比较以确定α是否是δαε的句柄,以及产生方式A→α是否是唯一可进行归约的产生式。弗洛伊德经过研究,给出其充分必要条件为:β和δ的最后m个符号相同,丁和o/的最初n个终结符相同。这样一个上下文无关文法G就称为(m,n)限界上下文文法。
在算法方面,弗洛伊德和威廉姆斯(J.Williams)在1964年共同发明了著名的堆排序算法HEAPSORT,这是与英国学者霍尔(C.A.R.Hoare,1980年图灵奖获得者)发明的QUICKSORT齐名的高效排序算法之一。此外还有直接以弗洛伊德命名的求最短路的算法,这是弗洛伊德利用动态规划(dynamic programming)的原理设计的一个高效算法。
在程序设计方面,计算机科学家非常关心的一个重要问题是如何表达和描述程序的逻辑,如何验证程序的正确性。1967年,在美国数学会AMS举行的应用数学讨论会上,弗洛伊德发表了那篇引起轰动并产生了深远影响的论文,即“如何确定程序的意义”(Assigning Meanings to Programs)。这篇论文在程序逻辑研究的历史上,是继麦卡锡(J.McCarthy,1971年图灵奖获得者)在1963年提出用递归函数作为程序的模型这一方法以后最重大的一个进展。麦卡锡倡导的方法对于一般程序,包括大型软件确实是行之有效的,但它有一个不足,即对于许多以命令方式编写的软件,其中包括赋值语句,条件语句,用While实现循环的语句……对这样的程序用递归定义的函数去证明其正确性就很不方便了。正是为了解决这个问题,弗洛伊德在上述论文中提出了一种基于流程图的表达程序逻辑的方法。这个方法的主要特点就是在流程图的每一弧线上放置一个“标记”(tag),也就是一个逻辑断言,并且保证只要当控制经过这个弧线时该断言一定成立。弗洛伊德的主要贡献在于解决了基于这种标记的形式系统的细节,证明了这种系统的完备性,解决了如何证明程序终结的问题。弗洛伊德还引入了验证条件的概念,包括流程图的一个组成部分(方框、圆框等)及其人口和出口处的标记。为了证明带标记的流程图的正确性,只要证明其中每一组成部分的验证条件成立就行了。弗洛伊德提出的方法被叫做“归纳断言法”(inductive assertion method),或前后断言法(pre·and post-assertion method)。在框图每个断点i上所加的逻辑断言即标记就叫i点的归纳断言,说明程序执行经过此点时在各输入变量x和各程序变量丁之间应存在的关系,以谓词Pi(x,y)的形式表示。若程序从断点i经过路段。到下一断点j的验证条件以Ra(x,y)表示,丁的值在。上的变化以ha(x,y)表示,则只要能证明下式恒真:
(∨x)(∨y)[pi(x,y)∧Ra(x,y) Pj(x,ha(x,y))]
程序从i到j的部分正确性也就证明了。
虽然用归纳断言法不能证明程序的完全正确性,因为它必须以程序能够终结为前提,但由于弗洛伊德在论文中同时也考虑了如何证明程序终结的问题,因此弗洛伊德的归纳断言法也就有了普遍的意义。
弗洛伊德在同年发表于《ACM学报》(Journal of ACM)10月号上的另一篇论文中,还第一次把“不确定性”概念引入程序。所谓“不确定性程序”(non deterministic program)就是根据操作规则有多种操作可供选择,而只选其中之一搜索下去的程序。这对人工智能问题的研究具有十分重要的意义。
此外,弗洛伊德还和伊万斯(R.0.Evans,因设计世界上第一个类比推理程序Analogy而闻名于世的学者。Analogy是可以判定几何图形是否类似的人工智能程序)一起设计了一种称为产生式语言的特殊的程序设计语言FPL(Floyd-Evans Production Language),用来编写计算机语言的语法分析程序。之所以称它为产生式语言,是因为用它编写的程序由一系列产生式(或称归约式)组成。实际上,用FPL编好语法分析程序以后,如果再插入语义子程序,就可以构成一个完整的编译器。用FPL语言编写的程序简称PP程序,由以下5个部分按自左至右顺序组成:
1.标号(可有可无);
2.栈顶符号串;
3.前看符号串(或称窗口符号串);
4.归约符号;
5.语义动作。
执行一个PP程序的方法是:依次检视各PP的第三部分。若某PP的第三部分和输入的前看符号串一致,则进一步检视此PP的第四部分,若非空,表示要进行归约,此时把它的第二部分和当前实际的栈顶符号串相比。如果能匹配上,则实行归约,即删去实际的栈顶符号串,用第四部分代替之,然后执行第五部分的动作。若此PP的第四部分为空,表示当前无归约可做,直接执行第五部分的动作即可。
弗洛伊德是1978年12月4日在华盛顿举行的ACM年会上接受图灵奖的。他发表了题为“程序设计的风范”(The Paradigms of Programming)的演说。演说全文刊于Communications of ACM,1979年8月,455-460页,也可见《前20年的ACM图灵奖演说集》(ACM Turing Award Lectures——The First 20Years:1966—1985,ACM Pr.),131—142页。弗洛伊德在演说中对结构化程序设计,递归协同例程(recursive coroutine),动态程序设计,基于规则的系统,状态变换机制(state-transition mechanism)等各种不同程序设计风范进行了比较,并介绍了自己在研究工作中如何根据具体情况应用不同风范的例子,很给人以启示。时间虽然已过去20多年,他的例子也许有些过时,但他的观点至今仍然是有效的。
罗伯特·弗洛伊德(Robert·Floyd)1936年生于纽约。他是芝加哥大学的毕业生,但学的不是数学或电气工程等与计算机密切相关的专业,而是文学,1953年获得文学学士学位。弗洛伊德在计算机科学的诸多领域,诸如算法、程序设计语言的逻辑和语义、自动程序综合、自动程序验证、编译器的理论和实现等方面都作出创造性的贡献。在算法方面,弗洛伊德在1964年发明了著名的堆排序算法。此外还有直接以弗洛伊德命名的求最短路径的算法,这是弗洛伊德利用动态规划的原理设计的一个高效算法。
元范式编辑本段回目录
1978年的图灵奖(Turing Award)授给了斯担福大学的Robert W. Floyd 。他授奖演说的题目是《编程的种种范式》,刊登在1979年8月的《ACM通讯》(Communications of the ACM)杂志上。
一种范式是一种模式——对于编程来说,也就是一种思考模式。Floyd利用领奖的机会向大家展示了他自己内心的工作机制——也许这能叫做一种“元范式”。可以提炼以下内容。
1.使用类比,把计算机的处理过程与人类机构中的处理过程联系起来,对比研究。
2.在解决复杂的问题时,并不是仅仅得到一个解法就满足了,而是反复追溯自己的思路;
3.从特殊案例中推出普遍规则,并且利用其他特殊案例来检验这些普遍规则。
4.阅读其他人的范式;
5.阅读别人的程序,尽量扩展自己的理解能力,专门去读懂那些“写法奇特”的人的代码,从而在读程序时取得更多的收获;
6.尝试跟别人交流范式,或者把自己的范式教给别人,以此进一步澄清自己的思想;
7.积极地调查别人此前的工作成果,而不是重新发明一切;
8.把别人的工作看做一个出发点,就此对自己提问:“我会怎样发明这个东西?”
Robert Floyd简介编辑本段回目录
Robert Floyd生于1936年6月8日美国纽约,去世于2001年9月25日。Robert从小就被视为神童,14岁就完成了其中学教育,然后进入芝加哥大学,并在年仅17岁时(1953年)就获得其文学学士学位。1958年,Robert获得了其第二个学士学位,专业为物理。20世纪60年代,Robert从事与计算机的工作并发表了许多著名的文章,Floyd的研究方向包括以寻求网络最短路径的运算法则的设计和分析、浮点运算、点阵打印机的灰度打印阴影、信息索引和随机交换与聚合的筛选等。其中,Floyd的最重要的科学成就是开创了程序检验的系统方法论。1967年,他的启蒙性论文Assigning Meaning to Programs开创了程序检验新方法。他的基本想法是在逻辑分置表中附加所谓的“标记”,以此来区别程序描述或分支,以定义基于常用程序语言的定义程序效果。世界范围内众多的计算方法研究人员采纳了他的观点。同时,Floyd还是代码重构——基本理念是重新改写程序,只保留程序基本概念——的第一位倡导者。重构是目前计算机编程中的基本操作。Robert在程序验证方面的开创性研究对后来程序验证领域著名的Hoare Logic有很大的积极影响作用,这也是为什么我们也通常称Hoare Logic叫做Floyd-Hoare Logic。Hoare是其在1969年发表的 “An axiomatic basis for computer programming”中的概念。年仅27时,他被CMU聘请为副教授一职。6年后,获得了斯坦福大学的终身教授的职务。在斯坦福大学,Robert与Donald Knuth成为同事和亲密的朋友,并长期紧密合作。1978年Robert W. Floyd被授予图灵奖,以表彰其在高效和可靠性软件设计方法学领域的显著影响;表彰其在下列计算机科学重要分支的奠基性的贡献:(词法)分析理论,编程语言语义,自动程序验证,自动程序综合生成和算法分析。此外,他还是前后断言法的创始人。