Categorical model of structural operational semantics for imperative language

Authors

  • William Steingartner Department of Computers and Informatics Faculty of Electrical Engineering and Informatics Technical University of Košice
  • Valerie Novitzká Department of Computers and Informatics Faculty of Electrical Engineering and Informatics Technical University of Košice

DOI:

https://doi.org/10.31341/jios.40.2.3

Keywords:

category theory, morphism, semantic function, state, structural operational semantics

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.

Downloads

Published

2016-12-09

How to Cite

[1]
W. Steingartner and V. Novitzká, “Categorical model of structural operational semantics for imperative language”, J. inf. organ. sci. (Online), vol. 40, no. 2, Dec. 2016.

Issue

Section

Articles