Tony Hoare - Tony Hoare

Herr

Tony Hoare

Sir Tony Hoare IMG 5125.jpg
Tony Hoare i 2011
Født
Charles Antony Richard Hoare

( 1934-01-11 )11. januar 1934 (87 år)
Andre navn CAR Hoare
Alma mater
Kjent for
Utmerkelser
Vitenskapelig karriere
Enger Informatikk
Institusjoner
Doktorgradsstudenter
Nettsted www .cs .ox .ac .uk /people /tony .hoare

Sir Charles Antony Richard Hoare FRS FREng (født 11. januar 1934) er en britisk informatiker .

Tony Hoare utviklet sorteringsalgoritmen quicksort i 1959–1960. Han utviklet også Hoare -logikk for å verifisere korrekthet av programmet, og det formelle språket som kommuniserer sekvensielle prosesser (CSP) for å spesifisere samspillet mellom samtidige prosesser (inkludert spisefilosofer -problemet ) og inspirasjonen til programmeringsspråket occam .

Hoare ble valgt til medlem av National Academy of Engineering i 2006 for grunnleggende bidrag til informatikk innen algoritmer, operativsystemer og programmeringsspråk.

Utdanning og tidlig liv

Tony Hoare ble født i Colombo , Ceylon (nå Sri Lanka ) av britiske foreldre; faren var en kolonial embetsmann og moren var datter av en teplanter. Hoare ble utdannet i England ved Dragon School i Oxford og King's School i Canterbury . Deretter studerte han Classics and Philosophy ("Greats") ved Merton College, Oxford . Da han ble uteksaminert i 1956 gjorde han 18 måneder nasjonal tjeneste i Royal Navy , hvor han lærte russisk. Han returnerte til University of Oxford i 1958 for å studere for et doktorgradssertifikat i statistikk , og det var her han begynte med dataprogrammering , etter å ha blitt undervist i AutocodeFerranti Mercury av Leslie Fox . Deretter dro han til Moscow State University som en utvekslingsstudent ved British Council , hvor han studerte maskinoversettelse under Andrey Kolmogorov .

Forskning og karriere

I 1960 forlot Hoare Sovjetunionen og begynte å jobbe hos Elliott Brothers Ltd , et lite dataproduksjonsfirma i London. Der implementerte han språket ALGOL 60 og begynte å utvikle store algoritmer .

Han var involvert i å utvikle internasjonale standarder innen programmering og informatikk, som medlem av International Federation for Information Processing (IFIP) Working Group 2.1 on Algorithmic Languages ​​and Calculi, som spesifiserte , vedlikeholder og støtter språkene ALGOL 60 og ALGOL 68 .

Han ble professor i datavitenskap ved Queen's University of Belfast i 1968, og i 1977 kom han tilbake til Oxford som professor i databehandling for å lede Programming Research Group i Oxford University Computing Laboratory (nå Institutt for informatikk, University of Oxford ) , etter Christopher Stracheys død . Han er nå emeritusprofessor der, og er også hovedforsker ved Microsoft Research i Cambridge , England.

Hoare mest betydelige arbeid har vært i følgende områder: hans sortering og utvalg algoritme ( quicksort og Quickselect ), Hoare logikk , formspråket kommuniserer sekvensielle prosesser (CSP) som brukes til å angi samspillet mellom samtidige prosesser , strukturering data operativsystemer bruker monitor konseptet, og den aksiomatiske spesifikasjonen av programmeringsspråk .

Beklager og trekker tilbake

Tony Hoare snakket på en programvarekonferanse i 2009 og beklaget at han fant opp null -referansen :

Jeg kaller det min milliardfeil. Det var oppfinnelsen av nullreferansen i 1965. På den tiden utformet jeg det første omfattende typesystemet for referanser i et objektorientert språk ( ALGOL W ). Målet mitt var å sikre at all bruk av referanser skulle være helt trygg, med kontroll utført automatisk av kompilatoren. Men jeg kunne ikke motstå fristelsen til å legge inn en null referanse, rett og slett fordi den var så enkel å implementere. Dette har ført til utallige feil, sårbarheter og systemkrasj, som sannsynligvis har forårsaket en milliard dollar med smerte og skade de siste førti årene.

For mange år under hans ledelse, Hoare Oxford avdeling jobbet på formell spesifikasjon språk som CSP og Z . Disse oppnådde ikke forventet inntak fra industrien, og i 1995 ble Hoare ført til å reflektere over de opprinnelige forutsetningene:

For ti år siden spådde forskere om formelle metoder (og jeg var den mest feilaktige blant dem) at programmeringsverdenen med takknemlighet ville omfavne enhver hjelp som ble lovet ved formalisering for å løse problemene med pålitelighet som oppstår når programmer blir store og mer sikkerhetskritiske. Programmer har nå blitt veldig store og veldig kritiske - langt utover omfanget som kan håndteres komfortabelt med formelle metoder. Det har vært mange problemer og feil, men disse har nesten alltid blitt tilskrevet mangelfull analyse av krav eller utilstrekkelig ledelseskontroll. Det har vist seg at verden bare ikke lider nevneverdig av den typen problemer som forskningen vår opprinnelig var ment å løse.

Bøker

  • Dahl, O.-J. ; Dijkstra, EW ; Hoare, CAR (1972). Strukturert programmering . Academic Press . ISBN 978-0-12-200550-3. OCLC  23937947 .
  • CAR Hoare (1985). Kommunisere sekvensielle prosesser . Prentice Hall International Series in Computer Science. ISBN  978-0131532717 (innbundet) eller ISBN  978-0131532892 (pocketbok). (Tilgjengelig online på http://www.usingcsp.com/ i PDF -format.)
  • Hoare, CAR; Gordon, MJC (1992). Mekanisert resonnement og maskinvaredesign . Prentice Hall International Series in Computer Science. ISBN 978-0-13-572405-7. OCLC  25712842 .
  • Hoare, CAR; Han, Jifeng (1998). Samlende teorier om programmering . Prentice Hall International Series in Computer Science. ISBN 978-0-13-458761-5. OCLC  38199961 .

Personlig

I 1962 giftet Hoare seg med Jill Pym, medlem av hans forskerteam.

Utmerkelser og æresbevisninger

Referanser

 Denne artikkelen inneholder tekst tilgjengelig under CC BY 4.0 -lisensen.

Eksterne linker