Ib Holm Sørensen

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.

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.

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. Han underviste tidligt i kurser i Z-notationen i Oxford.

Sørensen var leder af Transaktionsbehandlingsprojektet i Oxford fra starten i 1982 (senere omdøbt til "CICS Projektet"), i samarbejde med IBM (UK) Laboratorier. 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. 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).

Fra slutningen af 1980'erne var Sørensen central i udviklingen af B-metoden, en af de førende formelle metoder. Han forlod Oxford Universitet for at lede et hold for BP Research 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 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 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

Dataloger fra Danmark
Programmører fra Danmark
Personer fra Aabenraa
Ansatte ved Aarhus Universitet
Alumni fra University of Oxford
Ansatte ved University of Oxford
BP