托尼·霍尔博士Tony Hoare or
C.A.R. Hoare, born 11 January 1934
Tony Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth. During his National Service (1956-1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally) a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.
On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including his later wife Jill) in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of Chief Engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as Chief Scientist to the computing research division, where he worked on the hardware and software architecture for future machines.
These machines were cancelled when the Company merged with its rivals, and in 1968 Tony took a chance to apply for the Professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.
In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in Computer Science, including an external Master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.
Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.
分享到:
相关推荐
It shows how denotational semantics, operational semantics and algebraic semantics can be combined in a unified framework for the formal specification, design and implementation of programs and ...
A. R. Hoare)在1962年发表的关于快速排序算法的原始论文,题为 "Quicksort",发表在《The Computer Journal》第5卷第1期上。这篇论文是计算机科学领域的经典文献之一,首次详细介绍了快速排序算法的原理和实现方法...
资源有两份:一是中文电子版,周巢尘译的。中文版的通信顺序进程教材,主要有7章的内容。第一章是进程,第二章是并发性,第三章是非确定性,第四章是通信,第五章是顺序进程,第六章是资源...二是CSPbook_2004_Hoare。
A. R. Hoare(托尼·霍尔)撰写。本书首次出版于1985年,由Prentice Hall International发行,自问世以来便成为计算机科学理论与实践中的经典之作。托尼·霍尔不仅以其深刻的洞察力和严谨的学术态度著称,还因其在...
快速排序是一种高效的排序算法,由英国计算机科学家C.A.R. Hoare在1960年提出。它的基本思想是分治法(Divide and Conquer),通过选取一个基准元素,将待排序序列划分为两个子序列,使得一个子序列的所有元素都小于...
快速排序是一种高效的排序算法,由英国计算机科学家C.A.R. Hoare在1960年提出。该算法采用分治法(Divide and Conquer)的思想来实现,其基本步骤如下: 1. **选择基准元素**:从待排序的数组中选取一个元素作为...
霍尔逻辑(Hoare Logic)是一种用于形式化验证软件正确性的工具,由英国计算机科学家托尼·霍尔(C.A.R. Hoare)在1969年提出。它通过定义一套逻辑推导规则,来证明程序在给定的前置条件(Precondition)和后置条件...
A. R. Hoare在1962年提出。它的基本思想是:通过一趟排序将要排序的数据分割成独立的两部分,其中一部分的所有数据都比另外一部分的所有数据都要小,然后再按此方法对这两部分数据分别进行快速排序,整个排序过程...
THE Java™ programming language is a general-purpose, concurrent, classbased,... A. R. Hoare suggested in his classic paper on language design, the design has avoided including new and untested features.
A. R. Hoare在1960年代提出。它的核心思想是通过一个称为“基准元素”的选择与交换过程将待排序数组分成两个部分,其中一部分的所有元素都比另一部分的每一个元素要小(或大),然后递归地对这两部分再进行相同的...
日本程序员norahiko,写了一个排序算法的动画演示,非常有趣。排序算法(Sorting algorithm)是计算机科学最古老、最基本的课题之一。要想成为合格的程序员,就必须理解和... A. R. Hoare(1934--)于1960时提出来的
快速排序由C.A.R. Hoare在1960年提出,是应用最广泛的排序算法之一。它采用分治策略,通过选取一个基准元素,将数组分为两部分,一部分的所有元素都小于基准,另一部分的元素都大于基准,然后对这两部分递归地进行...
快速排序是一种高效的排序算法,由英国计算机科学家C.A.R. Hoare在1960年提出。它在很多情况下比其他基本排序算法如冒泡排序、插入排序等有着显著的性能优势,平均时间复杂度为O(n log n),在最坏情况下也能保持O(n^...
4. 快速排序:由C.A.R. Hoare提出的分治法策略,选取一个基准元素,将数组分为两部分,一部分的所有元素都小于基准,另一部分的所有元素都大于基准,然后对这两部分再分别进行快速排序。快速排序是目前最常用的内部...
快速排序由C.A.R. Hoare提出,采用分治策略,选取一个“基准”元素,将数组分为小于和大于基准的两部分,对这两部分递归执行相同操作。C语言实现的关键在于如何选择基准以及如何划分数组。 5. 归并排序(Merge Sort...
函数名称: qsort <br>函数原型: void qsort(void *base, size_t nelem, size_t width, int (*fcmp)(const void *,const void *) <br>函数功能: 使用C.A.R.Hoare排序法对数组base进行排序 <br>函数返回: ...
快速排序是一种高效的排序算法,由英国计算机科学家C.A.R. Hoare在1960年提出。它基于分治法(Divide and Conquer)策略,是C语言中常用的一种排序算法。本压缩包文件“C语言快速排序.zip”包含了关于如何在C语言中...
A. R. Hoare 在 1960 年提出。随机化快速排序基本思想:通过一趟排序将要排序的数据分割成独立的两部分,其中一部分的所有数据都比另外一部分的所有数据都要小,然后再按此方法对这两部分数据分别进行快速排序,...
该算法由C.A.R. Hoare在1960年提出,因此也被称为Hoare划分。算法实现原理:快速排序的基本思路是:选择一个基准元素,将数组划分为两个子数组,一个包含比基准元素小的元素,另一个包含比基准元素大的元素,然后...