Topics in structural operational semantics
Arnar Birgisson · 2009
Structural Operational Semantics (SOS) provides a mathematically rigourous way of specifying the semantics of formal (programming) languages. This thesis presents three individual contributions which highlight different uses of SOS and demonstrate how it may be used to benefit computer science. Together, the topics span a relatively wide spectrum, but their common theme is their use of SOS although each topic contains its own scientific contribution as well. In order, the topics range from practical applications of SOS to abstract meta-theory reasoning about SOS rules at a higher level. The first contribution relates to the use of operational semantics to specify the behaviour of a policy enforcement architecture built on top of transactional memory in Haskell. The second one discusses work in constructing a method for compositional reasoning about process calculi that includes a representation of the history of a computation, and allows the specification logic to look into the past. The final topic looks at SOS at a higher level, where we develop a rule format, which is a syntactic constraint on SOS rules that guarantees certain properties about the operators they define, namely determinism and idempotency.; Merkingarfraeði forrita ma skilgreina með Structural Operational Semantics (SOS) reglum. Slikar reglur veita staerðfraeðilega nakvaema leið til aðsetja fram merkingarfraeði (forritunar-) mala. Iþ essari ritgerð verða kynntþrju sjalfstaeð verkefni sem oll beita SOS með mismunandi haetti og sýna hvernig hagnýta ma formlega merkingafraeði. Saman spanna verkefnin breitt svið, en mynda heild i gegnum notkunþ eirra a SOS. Hvert verkefni inniheldurþo sjalfstaeða og nýja niðurstoðu a viðkomandi sviði. Iþ eirri roð sem verkefnin birtast er að finna allt fra hagnýtingu SOS viða ð skilgreina merkingarfraeði, til fraeðilegrar notkunar viða ð sanna almenn eigindi mala ohaðeinstokum malum. Fyrsta verkefnið fjallar um notkun formlegrar merkingarfraeði til aðskilgreina hegðun kerfis sem tryggir að oryggisreglur seu virtar við keyrslu forrits. Kerfið byggir a faersluminni (e. transactional memory) og er utfaert i Haskell. Annað verkefnið kynnir niðurstoður a sviði ferla-algebru sem inniheldur moguleika a að horfa a keyrslusogu ferla. Verkefnið kynnir aðferðir til að fjalla um eigindi fjolþraðakerfa a grundvelli eiginda einstakra ferla innanþ ess.Þrið ja og siðasta verkefniðsý nir almennt form fyrir SOS reglur, þannig að mal með merkingafraeði aþ vi formi uppfylla algebruleg skilyrði um einkvaema hegðun (e. deterministic behaviour) og sjalfvalda virkja (e. idempotent operators).