Axiomatizations from Structural Operational Semantics: Theory and Tools

Abstract

Structural Operational Semantics (SOS) is a well known standard for specifying language semantics in a natural, yet rigorous way. Once a formal way of checking for the equivalence of two programs written in such a language is provided, it is of great interest to derive efficient automated methods to prove if equivalences hold. Also of high interest for language designers is the possibility of enhancing the expressiveness of SOS in a formal manner, preserving as much from the already developed meta-theory of SOS as possible. The thesis focuses on these two areas, both from a theoretical and a practical perspective. The line of research addresses the extension of SOS with predicates and data, while lifting certain results from the meta-theory of SOS to these extensions. These results include automatically deriving axiomatizations for reasoning on program equivalence, and checking for compliance to rule formats in order to guarantee desired properties. Besides these extensions, the thesis provides an axiomatization for the coordination language Linda, presents a method to optimize axiomatizations for language constructs that are commutative, and presents a rule format for idempotent unary operators and idempotent terms. The practical aspect of this thesis consists of a core software framework for working with SOS meta-theories, named MetaSOS, which is implemented in Maude. The framework includes components for automatically deriving axiomatizations, performing simulations, and checking whether language constructs comply to a format for commutativity. It is designed in a modular and extensible fashion, and serves as a base for future implementations of other results from the meta-theory of SOS.

Þegar þróa á áreiðanlegan og stöðugan hugbúnaðar er oft fyrsta skerfið að lýsa á formlegan hátt hvað skilyrðum hann á að uppfylla. Þetta er gert með því að búa til formleg líkön af hugbúnaðinum sem nota má í þesum tilgangi . Það hefur verið vinsælt á síðari árum að nota líkön sem byggja a svokallaða uppbyggingarvinnslumerkingafræði, (á ensku "structural operational semantics en oftast vitnað til sem SOS) sem er fomlegur fræðilegur rammi (e. meta theory) til að lýsa eiginleikum formlega málsins sem kerfinu er lýst í. Á síðastliðnum árum hafa miklar rannsóknuir verið stundaðar og gera niðurstöður þeirra það mögulegt að segja til um eiginleika formlegra mála með því að líta á reglurnar sem lýsa merkingarfræði þeirra. I þessu doktorverkefni leggur höfundur sitt af mörkum til SOS fræðanna frá tveimur sjónarmiðum. Annars vegar hefur hann útvíkkað almennu fræðin með því að bæta við mikilvægum hugtökum sem ekki hefur verið fjallað um áður. Hins vegar hefur hann forritað kerfi, byggt á almennu fræðunum, þar sem hægt er að spyrja spurninga um ákveðin tilvik og fá svör við þeim. Þetta kerfi hefur fengið góðar undirtektir hjá væntanlegum notendum og er mikilvægt skref í áttina að nýtingu á rannsóknaniðurstöðum í greininni.