Formal semantics offers a complete and rigorous definition of a language. It is important to define different semantic models for a language and different models serve different purposes. Building equivalence between different semantic models of a language strengthen its formal foundation. This paper shows the derivation of denotational semantics from operational semantics of the language cCSP. The aim is to show the correspondence between operational and trace semantics. We extract traces from operational rules and use induction over traces to show the correspondence between the two semantics of cCSP.
Other than using induction, Hoare and He @cite_10 presented the idea of unifying different programming paradigms and showed how to derive operational semantics from its denotational presentation of a sequential language. They derive algebraic laws from the denotational definition and then derive the operational semantics from the algebraic laws. Similar to our work, Huibiao @cite_14 derived denotational semantics from operational semantics for a subset of Verilog @cite_9 . However the derivation was done in a different way than our method where the authors defined transitional condition and phase semantics from the operational semantics. The denotational semantics are derived from the sequential composition of the phase semantics. The authors also derived operational semantics from denotational semantics @cite_8 .
@cite_9 @cite_14 @cite_10 @cite_8
2107517480 1499638282 2110941259 2154982982
The Verilog hardware description language (HDL) is widely used to model the structure and behaviour of digital systems ranging from simple hardware building blocks to complete systems. Its semantics is based an the scheduling of events and the propagation of changes. Different Verilog models of the same device are used during the design process and it is important that these be 'equivalent'; formal methods for ensuring this could be commercially significant. Unfortunately, there is very little theory available to help. This self-contained tutorial paper explains the semantics of Verilog informally and poses a number of logical and semantic problems that are intended to provoke further research. Any theory developed to support Verilog is likely to be useful for the analysis of the similar (but more complex) language VHDL. In this paper operational equivalence of simple functional programs is defined, and certain basic theorems proved thereupon. These basic theorems include congruence, least fixed-point, an analogue to continuity, and fixed-point induction. We then show how any ordering on programs for which these theorems hold can be easily extended to give a fully abstract cpo for the language, giving evidence that any operational semantics with these basic theorems proven is complete with respect to a denotational semantics. Furthermore, the mathematical tools used in the paper are minimal, the techniques should be applicable to a wide class of languages, and all proofs are constructive. Professional practice in a mature engineering discipline is based on relevant scientific theories, usually expressed in the language of mathematics. A mathematical theory of programming aims to provide a similar basis for specification, design and implementation of computer programs. The theory can be presented in a variety of styles, including 1. Denotational, relating a program to a specification of its observable properties and behaviour. 2. Algebraic, providing equations and inequations for comparison, transformation and optimisation of designs and programs. 3. Operational, describing individual steps of a possible mechanical implementation. This paper presents simple theories of sequential non-deterministic programming in each of these three styles; by deriving each presentation from its predecessor in a cyclic fashion, mutual consistency is assured. This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.