Abstract
Distribuerte systemer består av et antall samarbeidende prosesser
som kjører på ulike maskiner og som kommuniserer med
meldingsutveklsing. Distribuerte systemer har blitt så vanlige at de
utgjør en del av samfunnets infrastruktur. Flere og flere kritiske
systemer er distribuerte. Kritiske systemer må være pålitelige og
korrekte.
Det er viktig at det er mulig å endre deler av et kritisk,
distribuert system på en god måte. Endringer må kunne skje
inkrementelt, det vil si i flere separate utviklingstrinn etter
hvert som behovene melder seg. I et objektorientert system er det
naturlig at endringer implementeres ved hjelp av arv. En typisk
situasjon vil være at vi ønsker å arve en klasse i systemet fordi vi
vil erstatte den med en subklasse med forbedret implementasjon eller
som tilbyr flere metoder.
Objekter i et distribuert system har behov for å synkronisere
interaksjonen sin. Arv av synkroniseringskode kan være problematisk.
I denne oppgaven brukes problemet med arveanomali som
eksempel på hvordan arv av synkroniseringskode fører til problemer
som ikke har noen tilfredsstillende løsning når vi bruker de
vanligste programmeringskonstruktene.
Creol er et lite språk som brukes til å studere
programmeringskonstrukter i en distribuert og objektorientert
kontekst. Creol har et forslag til hvordan problemene med arv av
synkroniseringskode kan løses på en bedre måte. Forslaget baserer
seg på bruken av et konstrukt som heter ``synkronisert fletting'',
som hittil bare har vært beskrevet uformelt. Den operasjonelle
semantikken til Creol er definert i det formelle spesifikasjons- og
modelleringsspråket Maude.
Hovedmålet for denne oppgaven er å videreutvikle og presisere
semantikken til synkronisert fletting med utgangspunkt i den
eksisterende, uformelle definisjonen. Jeg diskuterer ulike
semantiske tolkninger av både synkronisert fletting og to andre
beslektede programmeringskonstrukter. Dette resulterer i en
implementasjon av synkronisert fletting i språket Maude, som utvider
definisjonen av språket Creol.
Et sekundært mål for oppgaven er å gjøre en tentativ validering og
verifikasjon av implementasjonen. Dette gjøres med Maude sine
muligheter for maskinell analyse.
Som et eksempel på relatert arbeid i problemområdet, ser vi på
hvordan det aspektorienterte programmeringsparadigmet (AOP)
forholder seg til problemet med arveanomali.