🚀 go-pugleaf

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