Original scientific paper
https://doi.org/10.31341/jios.40.2.3
Categorical Model of Structural Operational Semantics for Imperative Language
William Steingartner
orcid.org/0000-0002-2852-9403
; Faculty of Electrical Engineering and Informatics, Technical university of Košice, Letná 9, 042 00 Košice, Slovak Republic
Valerie Novitzká
; Faculty of Electrical Engineering and Informatics, Technical university of Košice, Letná 9, 042 00 Košice, Slovak Republic
Abstract
Definition of programming languages consists of the formal definition of syntax and semantics. One of the most popular semantic methods used in various stages of software engineering is structural operational semantics. It describes program behavior in the form of state changes after execution of elementary steps of program. This feature makes structural operational semantics useful for implementation of programming languages and also for verification purposes. In our paper we present a new approach to structural operational semantics. We model behavior of programs in category of states, where objects are states, an abstraction of computer memory and morphisms model state changes, execution of a program in elementary steps. The advantage of using categorical model is its exact mathematical structure with many useful proved properties and its graphical illustration of program behavior as a path, i.e. a composition of morphisms. Our approach is able to accentuate dynamics of structural operational semantics. For simplicity, we assume that data are intuitively typed. Visualization and facility of our model is not only a new model of structural operational semantics of imperative programming languages but it can also serve for education purposes.
Keywords
category theory; morphism; semantic function; state; structural operational semantics
Hrčak ID:
170413
URI
Publication date:
9.12.2016.
Visits: 1.359 *