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 og . Han arbejdede i både den akademiske verden og industrien.Roscoe, Bill (8 February 2012). "Ib Sorensen – In memoriam". Department of Computer Science, University of Oxford, UK.
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 computer.Sørensen, Ib Holm; Kresse, Eric (December 1977). RIKKE-MATHILDA microassemblers and simulators on the DECSystem-10. Vol. DAIMI MD-28. Aarhus Universitet, Danmark. Karriere 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.Sørensen, Ib Holm (1981). Topics in programme specification and design: specification and design of distributed systems (DPhil). UK: Wolfson College, University of Oxford. Han underviste tidligt i kurser i Z-notationen i Oxford.Woodcock, Jim; Davies, Jim (1996). "Acknowledgments". Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall. .
Sørensen var leder af Transaktionsbehandlingsprojektet i Oxford fra starten i 1982 (senere omdøbt til "CICS Projektet"Fitzgerald, J. S. (October 2006). Perspectives on Formal Methods in the Last 25 years. Technical Report Series. Vol. CS-TR-983. UK: Newcastle University.), i samarbejde med IBM (UK) Laboratorier.Hayes, Ian (1993). "Preface to the first edition". Specification Case Studies. International Series in Computer Science (2nd ed.). Prentice Hall. . 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. 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.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. . Disse ideer blev senere formaliseret af i hans refinement kalkyle. 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).Hayes, Ian, ed. (1993). Specification Case Studies . International Series in Computer Science (2nd ed.). Prentice Hall. .
Fra slutningen af 1980'erne var Sørensen central i udviklingen af B-metoden, en af de førende formelle metoder.Bhattacharya, Sourav; Winter, Victor L., eds. (2012). "8. History of B". High Integrity Software. Springer. p. 40. . Han forlod Oxford Universitet for at lede et hold for BP ResearchCrichton, Edward (29 March 2022). "BToolkit". GitHub. 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-ToolkitWordsworth, J. B. (1996). Software Engineering With B. Addison-Wesley. . 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.
Udvalgte publikationer Ib Holm Sørensen var medforfatter til følgende:"Ib Holm Sorensen". Google Books."Ib Holm Sorensen". WorldCat.
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. . 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. . . 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. . (1st ed., 1987.)
Noter
Eksterne henvisninger Personlig hjemmeside Ib Holm Sørensen hos DBLP Bibliography Server Ib Sorensen på LinkedIn Ib Holm Sørensens videnskabelige bidrag på ResearchGate
Kategori:Dataloger fra Danmark Kategori:Programmører fra Danmark Kategori:Personer fra Aabenraa Kategori:Ansatte ved Aarhus Universitet Kategori:Alumni fra University of Oxford Kategori:Ansatte ved University of Oxford Kategori:BP