Ib Holm Sørensen

Fra Wikipedia, den frie encyklopædi
Ib Holm Sørensen
Født 29. januar 1949(1949-01-29)
Aabenraa, Danmark
Død 12. januar 2012 (62 år)
Fort-de-France, Martinique
Dødsårsag Slagtilfælde Rediger på Wikidata
Nationalitet Danmark Dansk
Uddannelse og virke
Uddannelses­sted University of Oxford
Akademisk vejleder Tony Hoare
Beskæftigelse Ingeniør, datalog Rediger på Wikidata
Forsknings­område Datalogi
Arbejdsgiver BP, University of Oxford, Aarhus Universitet Rediger på Wikidata
Arbejdssted Aarhus Universitet, University of Oxford, BP Research, B-Core (UK)
Kendt for formelle metoder, Z-notationen, B-metoden
Hovedværk B-Tool[1]
Påvirket af Jean-Raymond Abrial, Tony Hoare, Bernard Sufrin
Har påvirket Steve King, Carroll Morgan, Dave Neilson, Jim Woodcock
Nomineringer og priser
Information med symbolet Billede af blyant hentes fra Wikidata. Kildehenvisninger foreligger sammesteds.

Ib Holm Sørensen (født 29. januar 1949 – død 17. januar 2012) var en datalog, der bidrog til den tidlige udvikling og anvendelse af formelle metoder til specifikation af softwaresystemer og -moduler, især omkring Z-notationen (en) og B-metoden (en). Han arbejdede i både den akademiske verden og industrien.[4][5]

Han blev født i Aabenraa og startede sin akademisk karriere i 1970'erne ved Aarhus Universitet, hvor han arbejdede på Rikke-Mathilda mikro-assemblere og simulatorer på en DECSystem-10 (en) computer.[6]

Karriere[redigér | rediger kildetekst]

I 1979 kom Sørensen til programmeringsforskningsgruppen (PRG), en del af Oxford Universitets Computing Laboratory (nu Oxford Universitets Institut for Datalogi) i England, under ledelse af Tony Hoare. Der arbejdede han sammen med Jean-Raymond Abrial, Bernard Sufrin og andre i den tidlige udvikling af det formelle specifikationssprog Z. Han fik en DPhil-grad fra Oxford Universitet i 1981.[7] Han underviste tidligt i kurser i Z-notationen i Oxford.[8]

Sørensen var leder af Transaktionsbehandlingsprojektet i Oxford fra starten i 1982 (senere omdøbt til "CICS Projektet"[9]), i samarbejde med IBM (UK) Laboratorier.[10] Projektet specificerede formelt dele af IBMs CICS-transaktionsbehandlingssoftware ved hjælp af Z notationen. Dette vandt en Queen's Award for teknologisk præstation i 1992.[2][3] Som en del af CICS-projektet, udvidede han Edsger Dijkstras Guarded Command Language sprog ved at gøre det muligt at anvende Z-skema notationen som abstrakte kommandoer.[11] Disse ideer blev senere formaliseret af Carroll Morgan (en) i hans refinement kalkyle.[11] Sørensen var også medforfatter til den banebrydende Specification Case Study bog om brugen af Z, udgivet første gang i 1987 (anden udgave udkom i 1993).[12]

Fra slutningen af 1980'erne var Sørensen central i udviklingen af B-metoden, en af de førende formelle metoder.[13] Han forlod Oxford Universitet for at lede et hold for BP Research[13][1] for at udvikle B-værktøjet til at levere værktøjsstøtte til B-metoden. Han grundlagde derefter virksomheden B-Core (UK) Limited (nu nedlagt) til at støtte B-Toolkit[4][1][14] som er en samling af programmeringsværktøjer designet til at understøtte brugen af B-notationen, og han var med til at gennemføre en række B-relaterede projekter.

Senere vendte Sørensen tilbage til Oxford Universitet. Fra 1999 arbejdede han på de B-baserede Booster-modeller af krav. Han døde i 2012 inden han kunne gå på pension.[4]

Udvalgte publikationer[redigér | rediger kildetekst]

Ib Holm Sørensen var medforfatter til følgende:[15][16]

  • Ib Holm Sørensen, Eric Kressel (1975). A proposal for a multi-programming BCPL system on RIKKE-1 (på dansk). Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Eric Kressel, Ib Holm Sørensen (1975). The first BCPL system on RIKKE-1. Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Eric Kressel, Ib Holm Sørensen (1975). The Mathilda driver, a software tool for hardware testingb (på dansk). Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Ib Holm Sørensen, Eric Kressel (1977). DAIMI MD: RIKKE-MATHILDA microassemblers and simulators on the DECsystem 10. Vol. 28. Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Ib Holm Sørensen (1978). DAIMI PB: System Modelling: a Methodology for Describing the Structure of Complex Software, Firmware and Hardware Systems Consisting of Independent Process Components. Vol. 87. Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Jens Kristian Kjærgård, Ib Holm Sørensen (1980). DAIMI MD: BCPL on RIKKE (på dansk). Vol. 36. Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Jens Kristian Kjærgård, Ib Holm Sørensen (1980). DAIMI MD: The RIKKE Editor (på dansk). Vol. 37. Danmark: Matematisk Institut. Datalogisk Afdeling, Aarhus Universitet.
  • Ib Holm Sørensen (1981). DAIMI PB: Specification and Design of Distributed Systems. Danmark: Aarhus Universitet.
  • Ib Holm Sørensen (1981). Topics in programme specification and design: specification and design of distributed systems. DPhil thesis. UK: Wolfson College, University of Oxford.
  • Bill Flinn, Ib Holm Sørensen (1985). CAVIAR: A Case Study in Specification. UK: Programming Research Group Oxford University Computing Laboratory.
  • C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, B. A. Sufrin (August 1987). "Laws of programming". Communications of the ACM. 30 (8): 672–686. doi:10.1145/27651.27653.
  • Steve King, Ib Holm Sørensen, J. C. P. Woodcock (1988). Z: Grammar and Concrete and Abstract Syntaxes (Version 2.0). UK: Programming Research Group, Oxford University Computing Laboratory.
  • J.-R. Abrial, M. K. O. Lee, D. S. Neilson, P. N. Scharbach, I. H. Sørensen (1991). "The B-method". In S. Prehn, H. Toetenel (ed.). VDM '91 Formal Software Development Methods. Lecture Notes in Computer Science. Vol. 552. Berlin, Heidelberg: Springer. pp. 398–405. doi:10.1007/BFb0020001. ISBN 3-540-54868-8.
  • Bill Flynn, Roger Gimon, Steve King, Carroll Morgan, Ib Holm Sørensen, Bernard Surfrin (1993). Ian Hayes (ed.). Specification Case Studies. International Series in Computer Science (2nd ed.). Prentice Hall. ISBN 978-0-13-832544-2. (1st ed., 1987.)

Noter[redigér | rediger kildetekst]

  1. ^ a b c Crichton, Edward (29 March 2022). "BToolkit". GitHub.
  2. ^ a b King, Steve (1993). "The Use of Z in the Restructure of IBM CICS". In Hayes, Ian (ed.). Specification Case Studies. International Series in Computer Science (2nd ed.). Prentice Hall. pp. 202–213. ISBN 978-0-13-832544-2.
  3. ^ a b "Prof. Jim Woodcock, FREng" Arkiveret 3. oktober 2022 hos Wayback Machine. UK: University of York.
  4. ^ a b c Roscoe, Bill (8 February 2012). "Ib Sorensen – In memoriam". Department of Computer Science, University of Oxford, UK.
  5. ^ Bowen, Jonathan (juli 2022). "Ib Holm Sørensen: Ten Years After" (PDF). FACS FACTS (engelsk). No. 2022-2. BCS-FACS. s. 41-49. Hentet 3. august 2022.
  6. ^ Sørensen, Ib Holm; Kresse, Eric (December 1977). RIKKE-MATHILDA microassemblers and simulators on the DECSystem-10 (Webside ikke længere tilgængelig). Vol. DAIMI MD-28. Aarhus Universitet, Danmark.
  7. ^ Sørensen, Ib Holm (1981). Topics in programme specification and design: specification and design of distributed systems Arkiveret 31. juli 2022 hos Wayback Machine (DPhil). UK: Wolfson College, University of Oxford.
  8. ^ Woodcock, Jim; Davies, Jim (1996). "Acknowledgments". Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall. ISBN 0-13-948472-8.
  9. ^ Fitzgerald, J. S. (October 2006). Perspectives on Formal Methods in the Last 25 years. Technical Report Series. Vol. CS-TR-983. UK: Newcastle University.
  10. ^ Hayes, Ian (1993). "Preface to the first edition". Specification Case Studies. International Series in Computer Science (2nd ed.). Prentice Hall. ISBN 978-0-13-832544-2.
  11. ^ a b Hayes, Ian J.; King, Steve (2021). "11.9 Industry Influence on Research". In Jones, Cliff B.; Misra, Jayadev (eds.). Theories of Programming: The Life and Works of Tony Hoare. Association for Computing Machinery. pp. 266–267. ISBN 978-1-4503-8728-6.
  12. ^ Hayes, Ian, ed. (1993). Specification Case Studies. International Series in Computer Science (2nd ed.). Prentice Hall. ISBN 978-0-13-832544-2.
  13. ^ a b Bhattacharya, Sourav; Winter, Victor L., eds. (2012). "8. History of B". High Integrity Software. Springer. p. 40. ISBN 978-1461513919.
  14. ^ Wordsworth, J. B. (1996). Software Engineering With B. Addison-Wesley. ISBN 978-0201403565.
  15. ^ "Ib Holm Sorensen". Google Books.
  16. ^ "Ib Holm Sorensen". WorldCat.

Eksterne henvisninger[redigér | rediger kildetekst]

Hentet fra "https://da.wikipedia.org/w/index.php?title=Ib_Holm_Sørensen&oldid=11635103"