The paper presents a method of the development of operational semantics for imperative programming languages. It is based on the ontological approach to formal programming language specification implemented by information transition systems and conceptual transition systems. The method is illustrated by a fragment of the C language.
The methodology of the operational semantics development for programming languages based on the operational ontological approach, conceptual transition systems and CTSL, the language for the specification of such systems, is proposed. The development of operational semantics is illustrated by an example of procedural programming languages from the family MPL of...
The paper presents a new object model of domain-specific transition systems, a formalism designed for the specification and validation of formal methods for assuring software reliability. A formal definition of a model programming language is given on the basis of this model.
In the last decades, a number of stochastic enrichments of process algebras was constructed to specify stochastic processes within the well-developed framework of algebraic calculi. In [26], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed and called sPBC. The algebra sPBC has...
Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched with iteration. In this paper, we define a number of stochastic equivalences for dtsPBC which allow one to identify finite and infinite stochastic processes with similar behaviour. A problem of preservation of the...
Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement...