罗伯特·弗洛伊德的人物简介
(1936-2001)Robert W.Floyd
历届图灵奖得主基本上都有高学历、高学位,绝大多数有博士头衔。这是可以理解的,因为创新型人才需要有很好的文化素养,丰富的知识底蕴,因而必须接受良好的教育。但事情总有例外,1978年图灵奖获得者、斯坦福大学计算机科学系教授罗伯特·弗洛伊德就是一位“自学成才的计算机科学家”(a Self-Taught Computer Scientist)。
弗洛伊德1936年6月8日生于纽约。说他“自学成才”并不是说他没有接受过高等教育,他是芝加哥大学的毕业生,但学的不是数学或电气工程等与计算机密切相关的专业,而是文学,1953年获得文学士学位。
20世纪50年代初期美国经济不太景气,找工作比较困难,因学习文学而没有任何专门技能的弗洛伊德在就业上遇到很大麻烦,无奈之中到西屋电气公司当了二年计算机操作员,在IBM650机房值夜班。我们知道,早期的计算机都是以批处理方式工作的,计算机操作员的任务就是把程序员编写好的程序在卡片穿孔机(这是脱机的辅助外部设备)上穿成卡片,然后把卡片叠放在读卡机上输入计算机,以便运行程序。因此,操作员的工作比较简单,同打字员类似,不需要懂计算机,也不需要懂程序设计。但弗洛伊德毕竟是一个受过高等教育的人,又是一个有心人,干了一段时间的操作员,很快对计算机产生了兴趣,决心弄懂它,掌握它,于是他借了有关书籍资料在值班空闲时间刻苦学习钻研,有问题就虚心向程序员请教。白天不值班,他又回母校去听讲有关课程。这样,他不但在1958年又获得了理科学士学位,而且逐渐从计算机的门外汉变成计算机的行家里手。
1956年他离开西屋电气公司,到芝加哥的装甲研究基金会(Armour Research Foundation),开始还是当操作员,后来就当了程序员。1962年他被马萨诸塞州的Computer Associates公司聘为分析员。此时与Warsall合作发布Floyd-Warshall算法。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的部分正确性也就证明了。
虽然用归纳断言法不能证明程序的完全正确性,因为它必须以程序能够终结为前提,但由于弗洛伊德在论文中同时也考虑了如何证明程序终结的问题,因此弗洛伊德的归纳断言法也就有了普遍的意义。