Equivalence of formal semantics definition methods
Abstract
Abstract There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves. Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.
Related Papers
- → The Formal Semantics of Programming Languages(1993)652 cited
- → Operational and denotational semantics of prolog(1987)33 cited
- → Equivalence of formal semantics definition methods(1997)
- Equivalence proving of operational and denotational semantics about Repeat-until statement(2006)
- Semantics Transformation:From Direct Denotational Semantics to Continuation Denotational Semantics(2004)