Robert W. Floyd (06/08/1936—09/25/2001)

图 灵 奖 获 得 时 间 ：

1978年 。 第十三位 图 灵 奖 (1978年 ) 获 得 者 。

图 灵 奖 引 用 (Turing Award Citation) ：

Citation

For having a clear influence on methodologies for the creation of efficient and reliable software, and for helping to found the following important subfields of computer science: the theory of parsing, the semantics of programming languages, automatic program verification, automatic program synthesis, and analysis of algorithms.

中 文 翻 译 ：

” ( 授 予 Robert W. Floyd 图 灵 奖 以 表 彰 其 ) 在高效和可靠性软件设计方法学领域的显著影响；表彰其在下列计算机科学重要分支的奠基性的贡献：(词法)分析理论，编程语言语义，自动程序验证，自动程序综合生成和算法分析。

编 者 注 ：

关于软件可靠性领域的介绍，可参见：

http://www.ece.cmu.edu/~koopman/des_s99/sw_reliability/

关于程序语义学，可参见：

http://www.utdallas.edu/~gupta/alps/Proj_Desc/Wang.pdf

http://en.wikibooks.org/wiki/Computer_Science:Programming_Languages/Semantics_Specification

http://en.wikipedia.org/wiki/Semantics_of_programming_languages

关于编程语言领域研究实验室介绍，可参见：

http://www.cs.cmu.edu/~mleone/language/projects.html

关于程序验证(Program Verification), 其基本上是关于：

In computer science, program verification is the process of formally proving that a computer program does exactly what is stated in the program specification it was written to realize. It is an instance of formal verification (and more generally formal methods). Program verification is more specific in that it aims to verify the code itself, not only some abstract model of the program.

For functional programming languages, some programs can be verified by equational reasoning, usually together with induction. Code in an imperative language could be proved correct by use of Hoare logic.

读者也可阅读一些形式方法(Formal Methods)领域的一些介绍文章：

Important publications in formal verification  读者可以发现，Robert Floyd的著名文章：Assigning meanings to programs

列在首位。

http://en.wikipedia.org/wiki/Formal_verification

Formal Verification Reviews and Surveys: http://www.cerc.utexas.edu/~jay/fv_surveys/

Formal Methods Virtual Library: http://www.afm.sbu.ac.uk

斯坦福大学的Formal Verification研究小组：  http://verify.stanford.edu

Turing Award Lecture(图灵奖演讲文章)：

The Paradigms of Programming. Commun. ACM 22(8): 455-460(1979)

简 介 :

Robert Floyd生于1936年6月8日美国纽约，去世于2001年9月25日。

Robert从小就被视为神童，14岁就完成了其中学教育，然后进入芝加哥大学，并在年仅17岁时(1953年)就获得其文学学士学位。1958年，Robert获得了其第二个学士学位，专业为物理。

20世纪60年代，Robert从事与计算机的工作并发表了许多著名的文章，比如1967年发表的关于程序验证领域的前瞻性文章--Assigning Meanings to Programs.。Robert在程序验证方面的开创性研究对后来程序验证领域著名的Hoare Logic有很大的积极影响作用，这也是为什么我们也通常称Hoare Logic叫做Floyd-Hoare Logic。Hoare是在1969年发表其著名的 "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576━585, October 1969.

在Robert年仅27时，他被CMU聘请为副教授一职。6年后，获得了斯坦福大学的终身教授的职务。在斯坦福大学，Robert与Donald Knuth成为同事和亲密的朋友。

Robert与Donald Knuth长期紧密合作， 他是Knuth的“The Art of Computer Programming"一书的主要审稿人。

Robert W. Floyd Wiki: http://en.wikipedia.org/wiki/Robert_Floyd

斯坦福大学2001年11月7日关于Robert W. Floyd去世后发布的官方文章。值得注意的是，Robert是9月25日辞世的。

http://news-service.stanford.edu/news/2001/november7/floydobit-117.html

Donald Knuth写的悼念Robert Floyd的文章:

Robert W Floyd, In Memoriam by Donald E. Knuth, StanfordUniversity: http://sigact.acm.org/floyd/

Robert Floyd发表的论文:

• (with B. Ebstein) “A formal representation of the interference between several pulse trains,” Proceedings of the Fourth Conference on Radio Interference Reduction and Electronic Compatibility (Chicago: 1958), 180-192.
• “Remarks on a recent paper,” Communications of the ACM 2, 6 (June 1959), 21. “An algorithm defining ALGOL assignment statements,” Communications of the ACM 3 (1960), 170-171, 346.
• (with B. Kallick, C. J. Moore, and E. S. Schwartz) Advanced Studies of Computer Programming, ARF Project E121 (Chicago, Illinois: Armour Research Foundation of Illinois Institute of Technology, 15 July 1960), vi + 152 pages. [A description and user manual for the MOBIDIC Program Debugging System, including detailed flowcharts and program listings.]
• “A note on rational approximation,” Mathematics of Computation 14 (1960), 72-73.
• “Algorithm 18: Rational interpolation by continued fractions,” Communications of the ACM 3 (1960), 508.
• “An algorithm for coding efficient arithmetic operations,” Communications of the ACM 4 (1961), 42-51.
• “A descriptive language for symbol manipulation,” Journal of the Association for Computing Machinery 8 (1961), 579-584.
• “A note on mathematical induction on phrase structure grammars,” Information and Control 4 (1961), 353-358.
• “Algorithm 96: Ancestor,” Communications of the ACM 5 (1962), 344-345.
• “Algorithm 97: Shortest path,” Communications of the ACM 5 (1962), 345.
• “Algorithm 113: Treesort,” Communications of the ACM 5 (1962), 434.
• “On the nonexistence of a phrase structure grammar for ALGOL 60,” Communications of the ACM 5 (1962), 483-484.
• “On ambiguity in phrase structure languages,” Communications of the ACM 5 (1962), 526, 534.
• “Syntactic analysis and operator precedence,” Journal of the Association for Computing Machinery 10 (1963), 316-333.
• “Bounded context syntactic analysis,” Communications of the ACM 7 (1964), 62-67.
• “The syntax of programming languages--A survey,” IEEE Transactions on Electronic Computers EC-13 (1964), 346-353. Reprinted in Saul Rosen, Programming Languages and Systems (New York: McGraw-Hill, 1967), 342-358.
• “Algorithm 245: Treesort 3,” Communications of the ACM 7 (1964), 701.
• New Proofs of Old Theorems in Logic and Formal Linguistics (Pittsburgh, Pennsylvania: Carnegie Institute of Technology, November 1966), ii + 13 pages.
• (with Donald E. Knuth) “Advanced problem H-94,” Fibonacci Quarterly 4 (1966), 258.
• “Assigning meanings to programs,” Proceedings of Symposia in Applied Mathematics 19 (1967), 19-32.
• (with D. E. Knuth) “Improved constructions for the Bose-Nelson sorting problem,” Notices of the American Mathematical Society 14 (February 1967), 283.
• “The verifying compiler,”Computer Science Research Review (Pittsburgh, Pennsylvania: Carnegie-Mellon University, December 1967), 18-19.
• “Nondeterministic algorithms,” Journal of the Association for Computing Machinery 14 (1967), 636-644.
• (with Donald E. Knuth) “Notes on avoiding ‘go to’ statements,” Information Processing Letters 1 (1971), 23-31, 177. Reprinted in Writings of the Revolution, edited by E. Yourdon(New York: Yourdon Press, 1982), 153-162.
• “Toward interactive design of correct programs,” Information Processing 71, Proceedings of IFIP Congress 1971, 1 (Amsterdam: North-Holland, 1972), 7-10.
• (with James C. King) “An interpretation-oriented theorem prover over integers,” Journal of Computer and System Sciences 6 (1972), 305-323.
• “Permuting information in idealized two-level storage,” in Complexity of Computer Computations, edited by Raymond E. Miller and James W. Thatcher (New York: Plenum, 1972), 105-109.
• (with Donald E. Knuth) “The Bose-Nelson sorting problem,” in A Survey of Combinatorial Theory, edited by Jagdish N. Srivastava (Amsterdam: North-Holland, 1973), 163-172.
• (with Manuel Blum, VaughanPratt, Ronald L. Rivest, and Robert E. Tarjan) “Time bounds for selection,” Journal of Computer and System Sciences 7 (1973), 448-461.
• (with Alan J. Smith) “A linear time two tape merge,” Information Processing Letters 2 (1974), 123-125.
• (with Ronald L. Rivest) “Expected time bounds for selection,” Communications of the ACM 18 (1975), 165-172.
• (with Ronald L. Rivest) “Algorithm 489: The algorithm SELECT--for finding the ith smallest of n elements,” Communications of the ACM 18 (1975), 173.
• “The exact time required to perform generalized addition,” 16th Annual Symposium on Foundations of Computer Science (IEEE Computer Society, 1975), 3-5.
• (with Louis Steinberg) “An adaptive algorithm for spatial greyscale,” Proceedings of the Society for Information Display 17 (1976), 75-77. An earlier version appeared in SID 75 Digest (1975), 36-37.
• (with Larry Carter, John Gill, George Markowsky, and Mark Wegman) “Exact and approximate membership testers,” 10th Annual ACM Symposium on Theory of Computing (1978), 59-65.
• “The paradigms of programming,” Communications of the ACM 22 (1979), 455-460. Reprinted in ACM Turing Award Lectures: The First Twenty Years (New York: ACM Press, 1987), 131-142. Russian translation in Lektsii Laureatov Premii T’iuringa (Moscow: Mir, 1993), 159-173.
• (with Jeffrey D. Ullman) “The compilation of regular expressions into integrated circuits,” Journal of the Association for Computing Machinery 29 (1982), 603-622.
• (with Jon Bentley) “Programming pearls: A sample of brilliance,” Communications of the ACM 30 (1987), 754-757.
• “What else Pythagoras could have done,” American Mathematical Monthly 96 (1989), 67.
• (with Donald E. Knuth) “Addition machines,” SIAM Journal on Computing 19 (1990), 329-340.
• (with Richard Beigel) The Language of Machines (New York: Computer Science Press, 1994), xvii+ 706 pages. French translation by Daniel Krob, Le Langage des Machines (Paris: International Thomson, 1995), xvii+594 pages. German translation by Philip Zeitz and Carsten Grefe, Die Sprache der Maschinen (Bonn: International Thomson, 1996), xxvii + 652 pages.

Robert W. Floyd 历史照片: