🚀 go-pugleaf

song@minster.york.ac.uk writes:

>I am aware that there are four different styles to define semantics.
>	operational
>	denotational
>	algebraic 
>	axiomatic
>Could anyone give some comments on the following questions:
>	what is the relations among these semantics,
>	what is the purpose of each, 
>	any references on them
>	what is semantics defined in the CSP book

>Many thanks,

>Ji,

OK,

Firstly I have found the following to be useful references in
this particular area.

[Ada, 1980] "The Formal Definition of the Ada Programming Language", Honeywell Inc., 1980.
.XP
[Backus, 1960] "The Syntax and Semantics of the Proposed international Algerbraic Language of the Zurich ACM-GAMM
Conference", \fIInformation Processing\fP, UNESCO, Paris, pp. 125-132, 1960.
.XP
[Chomsky, 1959] "On Certain Formal Properties of Grammars", \fIInformation and Control\fP, \fI2\fP, pp. 137-167,
1959.
.XP
[Donahue, 1976] "Complimentary Definitions of Programming Language Semantics", Lecture Notes in Computer Science,
No. 42, Springer-Verlag, New-York, 1976.
.XP
[Dunlop et al., 1982] "A Comparative Analysis of Functional Correctness", ACM Computing Surveys, \fI14\fP, 2, pp.
229-244, 1982. 
.XP
[Gordon, 1979] "The Denotational Description of Programming Languages, An Introduction, Springer-Verlag, New-York,
1979.
.XP
[Hoare et al., 1973] "An Axiomatic Defintion of the Programming Language Pascal", \fIActa Informatica\fP, \fI2\fP,
pp. 335-355, 1973.
.XP
[Hoare et al., 1974] "Consistent and Complementary Formal Theories of the Semantics of Programming Languages",
\fIActa Informatica\fP, \fI3\fP, pp. 135-153, 1974.
.XP
[Lucas et al., 1969] "On the Formal Defintion of PL/I", \fI Ann. Rev. Auto. Prog.\fP, \fI6\fP, 3, pp. 105-182,
1969.
.XP
[Marcotty et al., 1976] "A Sampler of Formal Definitions", ACM Computing Surveys, \fI8\fP, 2, pp. 191-275, 1976.

Can I offer the following text as a description to the background and use of
theses formal semnatic methods. (Flame away). Honestly, I would appreciate
comments on this text. I used this in a report about a year ago (so I am not sure
that I would agree 100%, but I think it is not bad as a starter!). Comments ?  

.NH
Theoretical Models

.LP
The design and implementation of programming languages illustrates the complex interaction of theory and practice.
Many early language designs grew out of practical needs, with little or no input from theory. However, the
successes and failures of the early programming languages led to some early formal models of programming language
syntax and semantics, which in turn spawned better programming languages. These newer languages still contained a
number of design and implementation errors which required yet better theoretical models. Detailed below is a precis
of some of the major theoretical models that have had a significant impact upon the design and practice programming
languages.
.LP
It may be stated that theoretical models fall into two categories, namely qualitative or quantitative. Theoretical
models may be \fIqualitative\fP or \fIconceptual\fP, describing practice in terms of an underlying set of basic
concepts with not attempt made to provide any formal mathematical description of those concepts. Alternatively,
theoretical models may be \fIquantitative\fP or \fIformal\fP, describing practice in terms of a precise
mathematical model that can be studied, analyzed and manipulated using a series  of mathematical tools. A number of
formal models have been proposed for describing individual aspects of languages and their respective
implementations. A number of these theoretical models are described below.

.NH2
Formal grammars

.LP
The area of programming language design and implementation to receive some of the earliest attention was that of
syntax and translation. Within this area the class of theoretical models that have proved to be most useful are
defined as formal grammars. The BNF grammar is an example of a formal grammar. BNF consists of a set of productions
or grammar rules that recursively define a set of valid character sequences. The BNF grammar model was developed by
Backus and Naur for the description of the syntax of the ALGOL 60 programming language [Backus, 1960]. 

Another formal grammar was developed by the linguist Chomsky [Chomsky, 1959]. He developed a hierarchy of four
types of formal grammar, of which the context-free grammar bears a significant resemblance to the BNF grammar.
Another grammar, the regular grammar, was simpler than the BNF but however was unable to represent as complex a set
of constraints. However, the context-sensitive and unrestricted grammars developed by Chomsky were able to express
constraints that were beyond the ability of the BNF. 

Following Chomksy's pioneering work, numerous other formal grammars were developed, each exploring a different way
of defining the sort of constraints needed for actual programming languages. The context-sensitive and unrestricted
grammars, whilst being more powerful that BNF, turned out to be incorrect models for programming languages. Many
recent grammar forms have been developed in an attempt to overcome the limitations of these previous forms.

In practice, the description of the syntax of a new programming language is always routinely made using a formal
grammar. Most commonly some variant of BNF grammar is used for the definition, but often a more powerful form,
called a two-level grammar, is used. Theoretical studies have clarified the limits of BNF grammars and hence it is
now commonly understood that some classes of syntactic constraints cannot be described with them. Often, these are
described via attaching some informal notes to a BNF. The users of a language now routinely use a formal grammar to
answer questions about syntax. Implementors of a language also routinely use a formal grammar to generate a parser
for the language.

.NH2
Problems in Semantics

.LP
The definition of semantics in most programming language manuals is given in ordinary prose. In order to define the
syntax of a construct a production from a BNF or other formal grammar is provided. Added to this formal syntax is a
few paragraphs and (hopefully) a number of examples to define the semantics. Unfortunately it has been the case,
that the prose is ambiguous in meaning leading to different interpretations of the semantics of a language
construct. The consequences of such problems include may affect both programmer and implementor. Firstly, a
programmer may misunderstand what the program will do when executed and also an implementor may implement a program
construct in a manner different from other implementors of the same programming language. Hence, as with syntax,
methods are required to provide a precise, readable and concise definition of the semantics of a programming
language.

The problem of semantic definition has been a research topic for a considerable period. However, unlike the area of
syntactical definition, satisfactory solutions have been rare. Many different methods of formal definitions have
been developed and these may be subdivided into three general classes :-
.RS
.IP \(bu
Operational Methods
.IP \(bu
Denotational or Functional Methods and 
.IP \(bu
Axiomatic Methods.
.RE

.LP
\fBOperational methods\fP
.LP
An operational definition of a programming language is a definition organized around a formal model of how programs
in the language are executed on a virtual computer. It corresponds to an abstraction from the viewpoint of how the
language is implemented. The Vienna Definition Language is an example of an operational approach.

\fBDenotational methods\fP
.LP
A second class of semantic definition methods attempt to directly construct a definition of the function that each
program computes. The definition is built up hierarchically through definition of the function computed by each
individual program construct. Ultimately, a complete functional model of an entire program may be derived. The
method of \fIdenotational semantics\fP and the method of \fIfunctional semantics\fP are examples of this approach.

\fBAxiomatic methods\fP
.LP
A third class of methods for semantic definition define the semantics of each syntactic construct in the language
directly by giving an axiom or rule of inference that may be used to deduce the effect of execution of that
construct. In order to understand the meaning of an entire program it is necessary to use the axioms and rules of
inference in manner similar to ordinary proofs within the area of mathematics. The method of \fIaxiomatic
semantics\fP is an example of this method.

.NH3
Discussion

.LP
The various alternative semantic definition methods within each of these classes have provided the basis for
extensive formal study of issues relating to programming language semantics. The work of program correctness proofs
has been closely associated with the development of axiomatic semantics. Denotational semantics have provided the
basis for a deeper sense in which a program computes a function. Finally, operational semantics have led to
discovery of subtle issues in language implementations that are often not apparent to the language implementors.
semantic definition studies upon ition of most of Pascal is given by Hoare and Wirth [1973]. Donahue [1976] and
ml semantic definitions are becoming more an accepted part of the definition of new programming languages. One of
the requirements imposed during the definition of Ada was that a formal semantic definition was required for Ada.
The operational formal definition of PL/I was used as the basis for the standard PL/I definition; although it
should be added that the formal notation was not eventually retained within the standard. The effect of formal
semantic definition studies upon theoretical models of programming languages has not been as great as the effect of
formal grammars upon the definition of syntax. 

No single semantic definition method has been found useful for both user and implementor. The operational methods
often provide good formal models of implementation, but the definitions are often too detailed to be of value to an
user. Denotational methods do not provide much guidance to the implementor and have usually proven too complex to
be of direct value to the users. Axiomatic methods are more directly understandable by the language user, but
generally it has been found that they cannot be used to completely define a language without the definition
becoming extremely complex; providing little guidance to the implementor.

To date, the major impact of semantic definition of programming languages has been the use of such a definition
during the design of a language to detect and clarify subtle points that might lead to ambiguities in the language
definition. It should be noted however, that the final definition is still ordinarily presented using prose. The
denotational semantic definition of Ada was found to play a significant role in the development of the programming
language, yet only English prose and a BNF grammar are utilised to present the language formally.

.NH3
Literature

.LP
Marcotty et al. [1976] survey the issues relating to formal semantic definition and describe several methods.
Gordon [1979] provides an good introduction to denotational semantics. Dunlop and Basili [1982] describe Mills
functional semantics and contrast and compare it with denotational semantics. Lucas and Walk [1969] describe the
operational method called the Vienna Definition Language that was used for the formal definition of PL/I. A
denotational semantic definition of most of Ada is given in [Ada, 1980] and an axiomatic definition of most of
Pascal is given by Hoare and Wirth [1973]. Donahue [1976] and Hoare and Lauer [1974] contrasts these various
approaches and recommend a combination of equivalent definitions, each used for different purposes. 
Hoare and Lauer [1974] contrasts these various approaches and recommend a combination of equivalent definitions,
each used for different purposes.

Happy reading. Hopefully there are some pointers in there for you.

Regards

Brian

Brian J. King           | Voice: +44 91 222 8557  Fax: +44 91 261 1182  
Engineering Design Centre      | JANET: B.J.King@uk.ac.ncl 
The University          | Internet:B.J.King%newcastle.ac.uk@cunyvm.cuny.edu
Newcastle upon Tyne NE1 7RU UK | UUCP : ...!mcvax!ukc!ncl.ac.uk!B.J.King

Brian J. King        | Voice: +44 91 222 6000 ext 8558  Fax: +44 91 261 1182    
Engineering Design Centre      | JANET: B.J.King@uk.ac.ncl 
The University           | Internet:B.J.King%newcastle.ac.uk@cunyvm.cuny.edu
Newcastle upon Tyne NE1 7RU UK | UUCP : ...!mcvax!ukc!ncl.ac.uk!B.J.King