🚀 go-pugleaf

wm@uni-paderborn.de (Wolfgang Mueller) writes:


>I'm looking for any pointers to the formal semantics of ADA  
>preferring the classical denotational definition. Any other styles 
>are welcome as well.

>Thank you in advance.

>   wolfgang

What follows are excerpts from my Ph.D. proposal. I briefly discuss
VDM semantics, Petri Net semantics, Hoare-style axiomatic semantics,
and graph grammar semantics for Ada:

[VDM]

VDM has been used for providing Ada with a formal semantics [Ped87].
In general, A VDM semantic specification is broken into two parts: a
static semantics and a dynamic semantics. The static semantics define
what a syntactically 'meaningful' Ada program is e.g. with regards to
strong typing: an expression must have a type that is in complete
agreement with the context in which it appears. It is the task of the
Ada compiler front-end to ensure that the static semantics are abided
by. The dynamic semantics define the execution behavior of statically
'correct' Ada programs. One definition of Ada's dynamic semantics is
based on an approach called SMoLCS (Structured Monitored Linear
Concurrent Systems) that consists of two parts [AGM+86]. One part
defines terms that represent the possible states denoted by Ada
structures. The other part uses the notion of a labelled transition
system to define the operational semantics underlying the terms
defined in the first part. In this way, a compositional, operational
semantics for the complete Ada language has been defined. The
development of an interpreter for these dynamic semantics has been
is described in [FGI87,FGLT91]. The most recent of these publications
expresses pessimism concerning the practicality of utilizing their
interpreter. For example, they estimate that, based on experimental
results, a 1 second execution sequence of a compiled Ada program
running on a 1 MIPS computer, would take 23 days to execute using
their interpreter. These results are significant as they are the only
concrete results that have been published concerning the practicality
of interpreting the semantics of the entire Ada language. 

[Petri Nets]

In [MP89] a high-level Petri net model of Ada's operational semantics
is presented along with an algorithm for their interpretation. This
paper only describes the modelling of the Ada language tasking
primitives although the authors feel the rest of the language is
easily accommodated by their framework. 

[Hoare-style axioms]

In [GdR84] and [Coh86] a Hoare logic style proof system for a subset
of Ada is considered. As Hoare logic was originally intended to
provide semantics for transformational systems (as opposed to reactive
systems) this type of proof system is rather awkward.

[Graph Grammar]

A graph grammar approach to providing Ada with operational semantics
is presented in [Jac86]. In the words of the author, "the underlying
graph theoretic concepts are adequate for a full operational semantics
specification of Ada, though the work is restricted to the 'hard
kernel' of concurrency and synchronization."

References:

[Ped87]

@inproceedings{Pedersen87,
   author = {Jan Storbank Pedersen},
   booktitle = {VDM `87, VDM---A Formal Method at Work, VDM-Europe Symposium, Brussels, Belgium},
   editor = {D. Bjorner and C.B. Jones and M. Mac an Airchinnigh and E.J. Neuhold},
   month = mar,
   number = {252},
   pages = {33-48},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Computer Science},
   title = {{VDM} in Three Generations of {Ada} Formal Descriptions},
   year = {1987}
}

[AGM+86]

@inproceedings{AstesianoEtAl86,
   author = {E. Astesiano and A. Giovani and F. Mazzanti and G. Reggio and E. Zucca},
   booktitle = {{Ada}: Managing the Transition; Proceedings of the Ada-Europe International Conference, Edinburgh},
   editor = {Peter J.L. Wallis},
   month = may,
   pages = {239-248},
   publisher = {Cambridge University Press},
   title = {The {Ada} Challenge for New Formal Semantic  Techniques},
   year = {1986}
}

[FGLT91]

@article{FantechiEtAl91,
   author = {A. Fantechi and S. Gnesi and F. Leggio and P. Talini},
   journal = {ACM SIGPLAN Notices},
   month = mar,
   number = {3},
   pages = {25-34},
   title = {Executing the Formal Definition of {Ada}},
   volume = {26},
   year = {1991}
}

[FGI87]

@incollection{FantechiEtAl87,
   author = {A. Fantechi and S. Gnesi and P. Inverardi},
   booktitle = {Proceedings of the First European Software Engineering Conference (ESEC `87), Strasbourg},
   editor = {H.K. Nichols and D. Simpson},
   month = sep,
   number = {289},
   pages = {327-335},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Com Science},
   title = {An Execution Environment for the Formal Definition of {Ada}},
   year = {1987}
}

[MP89]

@incollection{MorascaPezze89,
   author = {Sandro Morasca and Mauro Pezze},
   booktitle = {Proceedings of the Second European Software Engineering Conference (ESEC `89), Coventry,UK},
   editor = {C. Ghezzi and J.A. McDermid},
   number = {387},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Computer Science},
   title = {Validation of Concurrent {Ada} Programs Using Symbolic Execution},
   year = {1989}
}

[GdR84]

@article{GerthDeRoever84,
   author = {Rob Gerth and Willem de Roever},
   journal = {Science of Computer Programming},
   pages = {159-204},
   title = {A Proof System for Concurrent {Ada} Programs},
   volume = {4},
   year = {1984}
}

[Coh86]

@inproceedings{Cohen86,
   author = {N.H. Cohen},
   booktitle = {{Ada}: Managing the Transition; Proceedings of the Ada-Europe International Conference, Edinburgh},
   editor = {Peter J.L. Wallis},
   pages = {229-238},
   publisher = {Cambridge University Press},
   title = {{Ada} Axiomatic Semantics: Problems and Solutions},
   year = {1986}
}

[Jac86]

@incollection{Jackel86,
   author = {Manfred Jackel},
   booktitle = {Graph Theoretic Concepts in Computer Science, Proceedings of the International Workshop WG `86, Bernried, FDR},
   editor = {Gottfried Tinhofer and Gunther Schmidt},
   month = jun,
   number = {246},
   pages = {41-57},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Computer Science},
   title = {{Ada} Concurrency Specified by Graph Grammars},
   year = {1986}
}
--
Greg Bond   ----->   bond@sce.carleton.ca  (613) 788 2600 (ext.1835)
Dept. of Systems and Computer Engineering, Carleton University
Ottawa, ON, Canada K1S 5B6