EnglishisÍslenska

Member institutions

Search in


ThesisReykjavík University>Tölvunarfræðideild>Meistaraprófsritgerðir>

Please use this identifier to cite or link to this item: http://hdl.handle.net/1946/7418

Titles
  • Topics in structural operational semantics

  • Formleg merkingarfræði og nýting hennar

Published
May 2009
Abstracts
  • 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.

  • is

    Merkingarfræði forrita má skilgreina með Structural Operational Semantics (SOS) reglum. Slíkar reglur veita stærðfræðilega nákvæma leið til aðsetja fram merkingarfræði (forritunar-) mála. Íþ essari ritgerð verða kynntþrjú sjálfstæð verkefni sem öll beita SOS með mismunandi hætti og sýna hvernig hagnýta má formlega merkingafræði. Saman spanna verkefnin breitt svið, en mynda heild í gegnum notkunþ eirra á SOS. Hvert verkefni inniheldurþó sjálfstæða og nýja niðurstöðu á viðkomandi sviði. Íþ eirri röð sem verkefnin birtast er að finna allt frá hagnýtingu SOS viða ð skilgreina merkingarfræði, til fræðilegrar notkunar viða ð sanna almenn eigindi mála óháðeinstökum málum.
    Fyrsta verkefnið fjallar um notkun formlegrar merkingarfræði til aðskilgreina hegðun kerfis sem tryggir að öryggisreglur séu virtar við keyrslu forrits. Kerfið byggir á færsluminni (e. transactional memory) og er útfært í Haskell. Annað verkefnið kynnir niðurstöður á sviði ferla-algebru sem inniheldur möguleika á að horfa á keyrslusögu ferla. Verkefnið kynnir aðferðir til að fjalla um eigindi fjölþráðakerfa á grundvelli eiginda einstakra ferla innanþ ess.Þrið ja og síðasta verkefniðsý nir almennt form fyrir SOS reglur, þannig að mál með merkingafræði áþ ví formi uppfylla algebruleg skilyrði um einkvæma hegðun (e. deterministic behaviour) og sjálfvalda virkja (e. idempotent operators).

Comments
is

Tölvunarfræði, Thesis

Issued Date
25/01/2011


Artifacts
Name[Sortable]Size[Sortable]Visibility[Sortable]Description[Sortable]Format
MSc_Arnar-Birgisson.pdf1.06MBOpen Complete Text PDF View/Open