The winners of previous Turing Awards are basically highly educated, and most of them have doctoral titles. This is understandable, because innovative talents need to have good cultural literacy and rich knowledge, so they must receive good education. But there are always exceptions. Robert Floyd, winner of 1978 Turing Award, is a computer science professor at Stanford University and a self-taught computer scientist.
Freud 1936 was born in new york on June 8th. To say that he is "self-taught" does not mean that he has not received higher education. He is a graduate of the University of Chicago, but he studied literature, not mathematics or electrical engineering closely related to computers. He received a Bachelor of Arts degree from 65438 to 0953.
In the early 1950s, the American economy was not very prosperous, so it was difficult to find a job. Freud, who had no special skills because he studied literature, was in great trouble in employment. In desperation, he worked as a computer operator in Westinghouse Electric Company for two years and worked at night shift in IBM650 computer room. As we know, early computers all worked in batch mode. The task of computer operators was to load the programs written by programmers into the cards on the card punch (an offline auxiliary external device), and then put the cards on the card reader and input them into the computer to run the programs. So the operator's job is relatively simple, similar to typist, and he doesn't need to know anything about computer and programming. But Freud was, after all, a highly educated man and an operator who had worked for some time. He soon became interested in computers and was determined to understand and master them. So he took advantage of his spare time on duty, borrowed relevant books and materials to study hard, and humbly asked the programmer for any questions. Not on duty during the day, he went back to his alma mater to listen to related courses. In this way, he not only obtained the bachelor of science degree from 1958, but also gradually became an expert in computer science from a layman.
From 65438 to 0956, he left Westinghouse and went to the Armor Research Foundation in Chicago. He started as an operator and later became a programmer. 1962 He was employed as an analyst by Computer Associates in Massachusetts. At this time, Floyd-Warshall algorithm was released in cooperation with Warsal. 1965 applied to be an associate professor at Carnegie Mellon University and transferred to Stanford University three years later. 1970 was hired as a professor.
The key to his rapid promotion lies in Freud's creative contributions in many fields of computer science through diligent study and in-depth research: algorithms, logic and semantics of programming languages, automatic program synthesis, automatic program verification and the theory and implementation of compilers. Including: 1962, Freud completed the development of Algol 60 compiler and successfully put it into use. This is one of the earliest Algol 60 compilers in the world. Freud took the lead in integrating optimization ideas in the development of this compiler, which made the compiled object code take up less space and run for a short time. Freud's thought of optimizing compilation has a far-reaching impact on the development of compilation technology. Subsequently, he made a systematic study of grammar analysis. Freud first put forward priority grammar and bounded context grammar. Priority grammar solves the primary task in bottom-up grammar analysis: how to find the "handle", that is, the symbol string that needs to be reduced at present. Freud solved this problem by defining different priorities for different symbols. The rule of binding contextual text is from the context-free grammar g:
*
S→βArβαγ
+
S→δαε
By comparison, it is determined whether α is the handle of δ α ε and whether production mode A→α is the only reducible production formula. After Freud's research, the necessary and sufficient conditions are as follows: the last m symbols of β and δ are the same, and the first n terminators of D and o/ are the same. Such a context-free grammar G is called (m, n) bounded context grammar.
In terms of algorithm, Freud and J. Williams invented the famous heap sorting algorithm HEAPSORT in 1964 * *, which is one of the efficient sorting algorithms with the same name as QUICKSORT invented by British scholar Hall (1980 Turing Prize winner). In addition, there is an algorithm named after Freud to find the shortest path, which is an efficient algorithm designed by Freud using the principle of dynamic programming.
In programming, computer scientists are very concerned about how to express and describe the logic of the program and how to verify the correctness of the program. 1967, at the seminar on applied mathematics held by AMS, the American Mathematical Society, Freud published a paper that caused a sensation and had a far-reaching impact, that is, how to give meaning to programs. In the history of program logic research, this paper is the most significant progress after j. McCarthy( 197 1 Turing Prize winner) put forward the method of using recursive function as the model of program in 1963.
The method advocated by McCarthy is indeed effective for general programs, including large-scale software, but it has one disadvantage, that is, it is inconvenient for many softwares written in command mode, including assignment statements, conditional statements, statements that use While loops ... to prove the correctness of such programs with recursively defined functions. In order to solve this problem, Freud proposed a program logic expression method based on flowchart in the above paper. The main feature of this method is to put a "tag" on each arc of the flow chart, that is, a logical assertion, and ensure that the assertion will be established as long as the control passes through this arc. Freud's main contribution lies in solving the details of the formal system based on this mark, proving the completeness of this system and solving the problem of how to prove the end of the program. Freud also introduced the concept of verification conditions, including a part of the flow chart (box, round box, etc.). ) and its population and exit signs. In order to prove the correctness of the marked flow chart, it is only necessary to prove that the verification conditions of each component are established. The method proposed by Freud is called "inductive assertion method" or "before and after assertion method". The logical assertion added at each breakpoint I in the block diagram is called point I inductive assertion, which explains the relationship between each input variable X and each program variable D when the program execution passes through this point, and is expressed in the form of predicate Pi(x, y). If the program passes through this section from breakpoint I, the verification condition to the next breakpoint J is expressed by Ra(x, y), and the value of d is in. The change in the figure is represented by ha(x, y), as long as the following formula can be proved:
(∨x)(∨y)[pi(x，y)∧Ra(x，y) Pj(x，ha(x，y))]
It also proves the partial correctness of the program from I to J.
Although inductive assertion cannot prove the complete correctness of the program, because it must be based on the premise that the program can be terminated, Freud also considered how to prove the termination of the program in his paper, so Freud's inductive assertion has universal significance.