Search

The formal semantics of programming languages forms the basis for many other formal methods used in software engineering. Its role is primarily in finding the meanings of programs and language constructs and in verifying the correctness of the design and implementation by means of formal procedures. Formal semantics has an irreplaceable place in the curricula of computer science and related fields of most universities. Its study requires a certain knowledge of mathematics and formal principles, therefore one of the results of our research is the visualization of semantic methods, primarily for educational purposes. In this article, we present an overview of our results in the field of definition and extension of semantic methods and their visualization. [ABSTRACT FROM AUTHOR]

Visualization of calculations in the field of semantic methods significantly contributes to a better understanding of the individual steps of the methods used. The use of virtual machines to design and prove the language properties is an important element in teaching compiler design. In this paper, we present visualization software that for a given input source in the model (toy) language Jane generates bytecode for an existing Computron virtual machine platform and a sequence of instructions for an abstract machine for operational semantics. [ABSTRACT FROM AUTHOR]

Semantics is concerned with the interpretation of programs written in some programming languages. The purpose of categorical semantics is to model how the computation is performed in categorical terms. Categories are mathematical structures with great illustrative power enabling to model also processes or computations. In this paper we extend our categorical semantics of simple imperative language Jane to named blocks - procedures. Semantics of procedures we define as a collection of categories interconnected by functors. Our approach enables nested declarations, repeated calls with different arguments and recursive calls without construction of the fixed point known from denotational approach. Such model allows to illustrate and accentuate the dynamics of categorical semantics. [ABSTRACT FROM AUTHOR]

Structural operational semantics is one of the most popular semantic methods in the community of software engineers. It describes program behavior in the form of change of states caused by execution of elementary steps. This feature predestinates Structural operational semantics for implementation of programming languages and also for verification purposes. In our paper we present a new approach to Structural operational semantics: behavior of programs, i.e. state changes we model in category of states. Category morphisms express elementary execution steps and program execution is an oriented path in category, i.e. composition of morphisms. Our approach is able to accentuate dynamics of Structural operational semantics, it is intuitively typed. That's why such model is suitable not only as a model for Structural operational semantics but also for educating young software engineers. [ABSTRACT FROM AUTHOR]

Programming in present can be characterized as a composition of some prepared components. New market was opened for providing components for various applications. However, every component library uses different standards, methods and requirements for using its products. Another problem is different terminology and a lack of some common standards. This situation can be compared with the period before setting open systems standards. We assume that analyzing of common principles of component programming can help to find unified formal description and it enables to construct formal models serving for solving and preventing troubles in composing appropriate components into working program systems. In our paper we try to present our analysis and preliminary ideas for achieving these aims. [ABSTRACT FROM AUTHOR]