Virkemidler for å støtte utviklingen av god programvare

Kvaliteten på programvare er viktig, spesielt med all digitaliseringen rundt oss. Bare i USA ble det i 2022 estimert et tap på over 2400 milliarder dollar på grunn av kvalitetssvikt i programvare. Dårlig programvare skaper problemer på flere områder. Apper lekker personopplysninger fordi sikkerheten svikter. En dårlig app gjør ikke det den skal og er vanskelig å bruke. Dårlig programvare sløser med naturressurser – alt fra apper som tapper batteriet på mobilen for strøm, til datasentre som bruker mye mer strøm enn nødvendig.

Å lage programvare av høy kvalitet er kostbart. Utviklerne mangler relevante tekniske hjelpemidler, og det er utfordrende å bevise at viktig kode er korrekt.

Vi studerer hvordan programmeringsspråket Magnolia kan støtte utviklingen av god programvare. Magnolia utvikles ved Bergen Language Design Laboratory (BLDL) på UiB. Det støtter formelle spesifikasjoner som gjør det mulig å bevise at kode er korrekt, og designes for å utforske gjenbruk av både kode og kodebevis. Gjenbruk av god kode øker programvarekvalitet og reduserer utviklingskostnader. Gjenbruk av bevis fordeler kostnadene ved å utvikle et bevis på mange applikasjoner.

Vi viser at Magnolias tilnærming til språkdesign og støtte for generisk programmering er et godt hjelpemiddel for gjenbruk av kode. Videre utforsker vi hvordan generisk programmering koblet med spesifikasjoner kan brukes til å bedre programvareytelse med eksempler fra tungregning. Tungregning er betegnelsen på de store beregningene innen naturvitenskap og teknologi, som for eksempel i klimaforskning. Vi bygger et sett av tekniske hjelpemidler som bruker spesifikasjoner, som er nyttige for bevis, til å automatisk bedre ytelsen til tungregning.

Resultatene viser at generisk programmering og formelle spesifikasjoner er kraftige virkemidler for å lage programvare av høy kvalitet og for å få ned kostnadene.

Personalia

Benjamin Chetioui (f. 1995) har en mastergrad i programvareutvikling fra Université de Strasbourg. Som doktorgradsstipendiat ble han veiledet av Jaakko Järvi (UiB/University of Turku) og Magne Haveraaen (UiB). Siden 2022 har han jobbet som kompilator-ingeniør ved Google.