Tony Hoare (Kolonbo, 1934ko urtarrilaren 11), Britainia Handiko informatikaria da, 1959-1960 urteetan quicksort izeneko ordenazio-algoritmoa garatu zuena. Sir Charles Antony Richard Hoare edo C. A. R. Hoare izenekin ere ezaguna da. Horretaz gain, programen zuzentasuna egiaztatzeko Hoare logika definitu zuen; prozesu konkurrenteen elkarrekintzak espezifikatzeko Communicating Sequential Processes (CSP) izeneko komunikazio-lengoaia garatu zuen, filosofoen afariaren problema ebazteko erabil daitekeena. Occam programazio-lengoaiaren inspiratzaile ere izan zen.[1]

Tony Hoare

(2011)
Bizitza
JaiotzaKolonbo1934ko urtarrilaren 11 (90 urte)
Herrialdea Erresuma Batua
BizilekuaCambridge
Familia
AitaHenry Samuel Malortie Hoare
AmaMarjorie Francis Villiers
Ezkontidea(k)Jill Pym (en) Itzuli
Hezkuntza
HeziketaMoskuko Estatu Unibertsitatea
Oxfordeko Unibertsitatea
Merton College (en) Itzuli
Dragon School (en) Itzuli
Tesi zuzendariaLeslie Fox (en) Itzuli
Doktorego ikaslea(k)Bill Roscoe (en) Itzuli
Cliff Jones (en) Itzuli
Augusto Sampaio (en) Itzuli
William James Stewart (en) Itzuli
Stephen D. Brookes (en) Itzuli
David Andrew Naumann (en) Itzuli
Andrew Philip Black (en) Itzuli
Peter Lauer (en) Itzuli
Jeremy Jacob (en) Itzuli
Masud Malik (en) Itzuli
John Elder (en) Itzuli
Jim (Wolfgang) Kaubisch (en) Itzuli
Richard Kennaway (en) Itzuli
T. Yung Kong (en) Itzuli
Geraint Jones (en) Itzuli
Christopher Dollin (en) Itzuli
Alex Teruel (en) Itzuli
Bryan Todd (en) Itzuli
Stephen Page (en) Itzuli
Clare Martin (en) Itzuli
Ken Wood (en) Itzuli
Stephen Brien (en) Itzuli
Paul Rudin (en) Itzuli
Hizkuntzakingelesa
Jarduerak
Jarduerakinformatikaria, ingeniaria, programatzailea, idazlea eta unibertsitateko irakaslea
Enplegatzailea(k)Microsoft
Oxfordeko Unibertsitatea
Belfasteko Queen's unibertsitatea
Lan nabarmenak
Jasotako sariak
KidetzaRoyal Society
Linzeen Akademia
Academia Europaea (en) Itzuli
Zientzien Bavariar Akademia
Ameriketako Estatu Batuetako Zientzien Akademia Nazionala
UK Computing Research Committee (en) Itzuli
cs.ox.ac.uk…

Formazioa eta gaztaroa aldatu

Ceilango Kolonbo herrian jaioa da (gaur egun Sri Lanka) guraso britainiarrekin. Hoare Ingalaterran hezi zen Oxford-eko Dragon School-en eta Canterburyko King 's School-en. Ondoren, Oxfordeko Unibertsitatean Kultura Klasikoa eta Filosofia Gradua lortu zuen. 1956an graduatu zenean, 18 hilabete egin zituen Royal Navy-n Zerbitzu Nazionalean, non errusiera ikasi zuen. Oxfordeko Unibertsitatera itzuli zen 1958an, estatistikako graduondoko baten ziurtagiria lortzeko, eta han hasi zen ordenagailuen programazioarekin. Ondoren, Moskuko Estatu Unibertsitatera joan zen British Councileko truke-ikasle bezala, non itzulpen automatikoa ikasi zuen Andrey Kolmogorovekin.

Ikerketak eta Karrera aldatu

 
Quicksort ordenazio-algoritmoa asmatu zuen.

1960an, Sobietar Batasuna utzi zuen eta Elliott Brothers Ltd enpresan hasi zen lanean. Bertan, ALGOL 60 lengoaia inplementatu zuen eta algoritmo nagusiak garatzen hasi zen. Informazioa Prozesatzeko Nazioarteko Federazioko (IFIP) 2.1 lan-taldeko kide izan zen, eta ALGOL 60 eta ALGOL 68 hizkuntzak babestu eta mantentzen ditu.

1968an Konputazio Zientzietako irakasle bihurtu zen Belfasteko Queen 's Unibertsitatean, eta 1977an Oxfordera itzuli zen konputazio irakasle gisa Programazio Talde Ikerketa zuzentzeko Oxfordeko Unibertsitatean Konputazio Laborategiko Programazioan (orain Informatika Saila, Oxfordeko Unibertsitatean), Christopher Strachey hil ondoren. Geroago irakasle emeritua izendatu zuten, eta Microsoft Researchen ikertzaile nagusia ere bada, Cambridgen (Ingalaterra).

Hoare-ren ekarpenik esanguratsuenak honako arlo hauetan egin dira:

  • Hoare-ren logika. 1969an, Floyd-en ideiak berreskuratuz, axioma eta inferentzia-erregelez osatutako sistema formala eratu zuen. Sistema horrek programen zuzentasun formala frogatzeko balio du eta asertzio diren inbarianteen metodoaren euskarria da. Geroztik programen zuzentasuna formalki frogatzeko zenbait metodo azaldu da, hala nola, "aldizkako asertzioena" edo semantika denotazionalean oinarritutakoa. Baina guztietan erabiliena Hoare-ren kalkulua izan da ezbairik gabe.[3][4]
  • Communicating sequential processes (CSP, prozesu sekuentzialen arteko komunikazioa) prozesu konkurrenteen arteko elkarreraginak zehazteko erabiltzen dena,
  • Konputagailuko sistema eragileak egituratuz monitore kontzeptua eta programazio-lengoaien espezifikazio axiomatikoa erabiliz.

Programa baten zuzentasuna frogatzen. Adibidea aldatu

 
Hoare-ren logika oinarria da programa informatikoen espezifikazio, egiaztapen eta eratorpen formala bderatzeko[4]

Hoare-ren logika oinarria da programa informatikoen espezifikazio, egiaztapen eta eratorpen formala bderatzeko. Hona hemen adibide xume bat, non egiaztatzen den if motako baldintzazko egitura batekin bi zenbakiren arteko kenduraren balio absolutua ondo kalkulatzen dela.[4]

Froga ezazu ondoko programak z aldagaian
x eta y-ren arteko kenduraren balio absolutua uzten duela:

--true
if x  y then
    z:=x-y; 
else
    z:=y-x; 
end if;
--z = |x-y|

1.- (x  y)  (x-y  0  x-y=x-y)
2.- {x-y  0  x-y=x-y} z:=x-y {x-y  0  z=x-y} (AA)
3.- (x-y  0  z=x-y)  (z = |x-y| )
4.- {x  y} z:=x-y {z = |x-y|} 1, 2, 3, (ODE)
5.- ¬(x  y)  (y-x = y-x  ¬(x  y))
6.-{(y-x = y-x  ¬(x  y)} z:=y-x {z = y-x  ¬(x  y)} (AA)
7.- (z = y-x  ¬(x  y))  (z = |x-y|)
8.-  x  y} z:=y-x {z = |x-y|} 5, 6, 7, (ODE)
9.- {true} if x  y then z:=x-y else z:=y-x {z = |x-y|}
                                          4, 8, (BDE)

Barkamenak eta atzera-egiteak aldatu

2009an egindako hitzaldi batean, Hoarek barkamena eskatu zuen erreferentzia nulua asmatu zuelako:[5]

Mila milioi dolarreko akatsa deitzen diot. Erreferentzia nuluaren asmakuntza izan zen hura 1965ean. Une hartan, erreferentziak egiteko lehen sistema integrala diseinatzen ari nintzen, objektuetara bideratutako lengoaia batean (ALGOL W). Nire helburua erreferentzien erabilera oro erabat segurua izatea zen, konpiladoreak automatikoki egindako egiaztapenekin. Baina ezin izan nion eutsi erreferentzia nulua ere jartzeko tentazioari, hain zen erraza inplementatzeko. Horren ondorioz, makina bat akats, ahultasun eta sistema-akats gertatu dira geroago, eta horrek mila miloi dolarreko mina eta kalteak eragin ditu azken berrogei urteetan.

Urte askoan, Oxfordeko bere departamenduak, bere zuzendaritzapean, espezifikazio formaleko lengoaietan lan egin zuen, CSP eta Zren moduko lengaietan. Sistema horiek ez zuten jaso espero zen moduko harrera industrian, eta 1995ean Hoarek jatorrizko hipotesiei buruz hausnartu behar izan zuen:

Duela hamar urte, metodo formaletako ikertzaileek (eta haien artean nahasietan nahasiena nintzen) iragarri zuten programazioaren munduak eskertuta hartuko zituela programak handiagoak bihurtzen direnean eta haien segurtasuna kritikoagoa denean sortzen diren fidagarritasun-arazoak konpontzeko formalizazioak agindutako laguntza guztiak. Orain, programak oso handiak eta kritikoak izatera iritsi dira - Metodo formalek eroso landu dezaketen eskalatik haratago. Arazo eta porrot asko egon ziren, baina ia beti baldintzen azterketa desegokiari edo kudeaketa-kontrol desegokiari egotzi ahal izan zaizkie. Egiaztatu da ezetz, munduak ez dituela modu esanguratsuan jasaten gure ikerketak jatorrian konpondu nahi zituen arazoak.

Liburuak aldatu

Bizitza pertsonala aldatu

1962an, Hoare Jill Pym-ekin ezkondu zen, bere ikerketa taldeko kide batekin.

Sariak eta ohoreak aldatu

Erreferentziak aldatu

  1. (Ingelesez) «Tony Hoare - Home» dl.acm.org (Noiz kontsultatua: 2020-04-30).
  2. Arruabarrena, Rosa. (1997). Algoritmika. UEU.
  3. Javier Alvez Gimenez, Xabier Arregi Iparragirre, Jose Gaintzarain Ibarmia, Paqui Lucio Carrasco, Montse Maritxalar Anglada. (2016). Programen espezifikazio, egiaztapen eta eratorpen formala. Udako Euskal Unibertsitatea ISBN 978-84-8438-590-5. PMC 974392192. (Noiz kontsultatua: 2020-06-04).
  4. a b c Iparragirre, Xabier Arregi; Sanchez, Arantza Diaz de Ilarraza; Carrasco, Paqui Lucio. (1993). Programen egiaztapena eta eratorpena. UEU arg ISBN 978-84-86967-50-5. (Noiz kontsultatua: 2020-06-04).
  5. (Ingelesez) «Null References: The Billion Dollar Mistake» InfoQ (Noiz kontsultatua: 2020-06-04).
  6. Hoare, Charles Antony Richard. «The emperor's old clothes» ACM Turing Award Lectures (Association of Computing Machinery): 1980. ISBN 978-1-4503-1049-9. (Noiz kontsultatua: 2020-04-30).
  7. Thrower, N. J. W.. (2003-01-22). «Samuel Pepys FRS (1633-1703) and The Royal Society» Notes and Records of the Royal Society of London 57 (1): 3–13.  doi:10.1098/rsnr.2003.0193. ISSN 1743-0178. (Noiz kontsultatua: 2020-04-30).
  8. Darby, Antony; Natarajan, Sukumar; Coley, David; Maskell, Dan; Walker, Ian; Brownjohn, James. (2019). Impact of sustainable building design on occupant experience: A human centred approach. Coventry University and The University of Wisconsin Milwaukee Centre for By-products Utilization  doi:10.18552/2019/idscmt5140. ISBN 978-1-0783-1443-5. (Noiz kontsultatua: 2020-04-30).
  9. Hoare, Sir (Charles) Antony (Richard), (Tony), (born 11 Jan. 1934), Principal Researcher, Microsoft Research Ltd, Cambridge, 1999–2015; Honorary Member, Cambridge University Computing Laboratory, since 2007. Oxford University Press 2007-12-01 (Noiz kontsultatua: 2020-05-02).
  10. «LIST OF PLATES» Euthymides and His Fellows (Harvard University Press) ISBN 978-0-674-33727-5. (Noiz kontsultatua: 2020-05-02).
  11. Krishfield, Richard; Honjoa, Susumu; Takizawa, Takatoshi; Hatakeyama, Kiyoshi. (1999). Ice-ocean environmental buoy program : archived data processing and graphical results from April 1992 through November 1998. Woods Hole Oceanographic Institution (Noiz kontsultatua: 2020-05-02).
  12. Burke, Richard, (29 March 1932–15 March 2016), President, Canon Foundation in Europe, 1988–98. Oxford University Press 2007-12-01 (Noiz kontsultatua: 2020-05-02).
  13. Jessen, Eike; Bauer, Friedrich L.. (2015-04). «Nachruf auf Eike Jessen und Friedrich L Bauer» IT-Szene München 10 (2): 9–9.  doi:10.1007/s40567-015-0016-0. ISSN 1863-1983. (Noiz kontsultatua: 2020-05-02).
  14. Hoare, Tony. (2012). «Message of thanks» Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '12 (ACM Press)  doi:10.1145/2103656.2103659. ISBN 978-1-4503-1083-3. (Noiz kontsultatua: 2020-05-02).
  15. «CAS centennial medal recipients» IEEE Circuits & Systems Magazine 6 (3): 16–16. 1984-09  doi:10.1109/mcas.1984.6323950. ISSN 0163-6812. (Noiz kontsultatua: 2020-05-02).
  16. Danecka, Daria; Olejarczyk, Ewa. (2014-10-16). «Profesor Wojciech Radecki Doktorem Honoris Causa Uniwersytetu Śląskiego» Przegląd Prawa Ochrony Środowiska (3)  doi:10.12775/ppos.2014.037. ISSN 2080-9506. (Noiz kontsultatua: 2020-05-02).
  17. Discursos de los Doctores Honoris Causa en la Universidad de Piura. Universidad de Piura 2019-08-30 (Noiz kontsultatua: 2020-05-02).

Kanpo estekak aldatu