is Íslenska en English

Lokaverkefni (Meistara)

Háskólinn í Reykjavík > Tæknisvið / School of Technology > MSc Tölvunarfræðideild / Department of Computer Science >

Vinsamlegast notið þetta auðkenni þegar þið vitnið til verksins eða tengið í það: http://hdl.handle.net/1946/7418

Titill: 
  • Titill er á ensku Topics in structural operational semantics
  • Formleg merkingarfræði og nýting hennar
Námsstig: 
  • Meistara
Leiðbeinandi: 
Útdráttur: 
  • Útdráttur er á ensku

    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.

  • 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).

Samþykkt: 
  • 25.1.2011
URI: 
  • http://hdl.handle.net/1946/7418


Skrár
Skráarnafn Stærð AðgangurLýsingSkráartegund 
MSc_Arnar-Birgisson.pdf1.04 MBOpinnHeildartextiPDFSkoða/Opna