🚀 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

In <1gidssINN14c@uni-paderborn.de> 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.

Some references off hand (mostly algebraically or partial correctness
oriented):

@article{C87MeldaC,
	author = "Meldal, S.",
	title = "A complete axiomatic semantics of spawning",
	journal = "Distributed Computing",
	year = "1991",
	volume = "5",
	pages = "159-174"
}

@article{C79LucPol,
	author = "Luckham, D. C. and Polak, W.",
	title = "Ada exception handling * An axiomatic approach",
	journal = "ACM TOPLAS",
	year = "1979",
	volume = "2"
}

@techreport{C84Anna__,
	title = "ANNA * A Language for Annotating Ada Programs",
	author = "Luckham, D. C. and von Henke, F. W. and Krieg-Bruckner, B. and Owe, O.",
	institution = "Stanford University, Tech. Report no. CSL-84-261",
	year = "1984"
}

@article{C85LucHen,
	author = "Luckham, D. C. and von Henke, F. W.",
	title = "An overview of Anna, a specification language for Ada",
	journal = "IEEE Software",
	year = "1985",
	volume = "2",
	number = "2",
	pages = "9*23"
}


@book{C82McGetr,
	title = "Program Verification Using Ada",
	publisher = "Cambridge Computer Science Texts, Cambridge University Press, Cambridge",
	year = "1982",
	author = "McGettrick, A. D. "
}

@techreport{C84ArunKu,
	title = "A Partial Correctness Proof System for Ada Tasks",
	author = "Arun-Kumar, S.",
	institution = "Tata Institute of Fundamental Research, CS-84/10",
	year = "1984"
}

@article{C84GerDeR,
	author = "Gerth, R. and de Roever, W. P.",
	title = "A proof system for concurrent Ada programs",
	journal = "Science of Computer Programming",
	year = "1984",
	volume = "4",
	pages = "159-204",
keyword = {Partial correctness, total correctness, ada, concurrency}
"
}

@book{BJOR81A,
	title = "Towards a Formal Description of Ada",
	publisher = "Springer-Verlag",
	year = "1981",
	author = "D. Bjorner"
}

@article{DONZ80A,
	author = "V.D. Donzeau-Gouge and G. Kahn and B. Lang",
	title = "Formal Definition of the Ada Programming Lanugage",
	journal = "IRIA",
	year = "1980",
	month = "November"
}

@inproceedings{LI82A,
	author = "W. Li",
	title = "An Operational Semantics of Multitasking and Exception Handling in Ada",
	booktitle = "Proceedings of the AdaTec Conference on Ada",
	year = "1982",
	organization = "ACM",
	pages = "138*151",
	address = "Arlington, Virginia",
	editor = "A.B. Gargaro",
	month = "October"
}

@inproceedings{LUCK80b,
	author = "D.C. Luckham and W. Polak",
	title = "A Practical Method of Documenting and Verifying Ada Programs with Packages",
	booktitle = "Proceedings of the Symposium on the Ada Programming Language",
	year = "1980",
	organization = "ACM",
	month = "November",
	note = "ACM SIGPLAN Notices 1511:113*122."
}

@inproceedings{LUCK86E,
	author = "D.C. Luckham and D.P. Helmbold and S. Meldal and D.L. Bryan and M.A. Haberler",
	title = "Task Sequencing Language for Specifying Distributed Ada Systems",
	booktitle = "System Development and Ada",
	year = "1987",
	publisher = "Springer-Verlag",
	volume = "LNCS # 259",
	pages = "249*305",
	note = "Presented at the CRAI Consorzio per le Ricerche e le Applicazioni di Informatica Workshop on Software Factories and Ada, Capri, Italy, May 26*30, 1986.",
	editor = {A.N. Habermann and U. Montanari}
}

@inproceedings{VHEN85A,
	author = "F.W. von Henke and D.C. Luckham and B. Krieg-Brueckner and O. Owe",
	title = "Semantic Specification of Ada Packages",
	booktitle = "Proceedings of the Ada International Conference",
	year = "1985",
	publisher = "Cambridge University Press",
	pages = "185*196",
	address = "Paris, France",
	month = "May 14*16",
	editor  = {J. Barnes and G. Fisher}
}

Then there are papers that use Ada or Ada mechanisms as examples within a more general setting. One such is

@article{SchlichtingSchneider84,
	author = "Richard D. Schlichting and Fred B. Schneider",
	title = "Using message passing for distributed programming: Proof rules and disciplines",
	journal = "ACM TOPLAS",
	year = "1984",
	volume = "6",
	number = "3",
	pages = "402*431",
	month = "July"
}
--
Department of Informatics | Internet:sigurd@ii.uib.no
HiB                       |          meldal@anna.stanford.edu
N - 5020 Bergen           | Phone:   +47 5 54 42 00
Norway                    | Fax:     +47 5 54 41 99