A language for systems not just software

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A language for systems not just software

Full text

Pdf (120 KB)

Source

Annual International Conference on Ada archive
Proceedings of the 2001 annual ACM SIGAda international conference on Ada table of contents

Bloomington, MN

SESSION: Plenary track table of contents

Pages: 3 - 11

Year of Publication: 2001

ISBN:1-58113-392-8

Also published in ...

Author

Peter Amey

Praxis Critical Systems, Bath, BA1 1PX, UK

Sponsor

SIGADA: ACM Special Interest Group on Ada Programming Language

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 9, Citation Count: 2

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/507574.507578 What is a DOI?

ABSTRACT

The specification and implementation of software-intensive systems have generally been viewed as separate processes with differing notations. There are good reasons for trying to use notations capable of bridging the gap between the two. The spark language was originally concerned solely with providing an unambiguous subset of Ada that was suitable for rigorous static analysis and formal verification. Evolution of spark's system of formal comments or annotations has resulted in a language which now provides parallel descriptions of required system behaviour and software implementation. Analyses performed by the spark Examiner bind these parallel descriptions together. The result, not foreseen by the original designers of spark, is a language that can be used to describe systems rather than just implement software.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Amey, Peter. The INFORMED Design Method for SPARK. Praxis Critical Systems 1999.
	2	Barnes, John. High Integrity Ada - the SPARK Approach. Addison Wesley Longman, ISBN 0-201-17517-7.
	3	Bramson, B. D. Malvern's Program Analysers. RSRE Research Review 1984.
	4	Carré, Bernard. Program Analysis and Verification in High Integrity Software. Sennett, Chris (Ed). Pitman. ISBN 0-273-03158-9.
	5	Chapman, R. C. Industrial Experience of SPARK. Proceeding of SIGAda 2000. http://www.acm.org/sigada/conf/sigada2000/
	6	Cooper, C. Daniel. Ada Code Analysis: Technology, Experience, and Issues. Proceeding of SIGAda 2000. http://www.acm.org/sigada/conf/sigada2000/
	7	Finnie, Gavin et al: SPARK - The SPADE Ada Kernel. Edition 3.3, 1997, Praxis Critical Systems
	8	Finnie, Gavin et al: SPARK 95 - The SPADE Ada 95 Kernel. 1999, Praxis Critical Systems
	9	Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
	10	David Lorge Parnas , Jan Madey, Functional documents for computer systems, Science of Computer Programming, v.25 n.1, p.41-61, Oct. 1995 [doi>10.1016/0167-6423(95)96871-J]
	11	Peter J. Robinson, Hierarchical object-oriented design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
	12	Alfred Rosskopf, Use of a Static Analysis Tool for Safety-Critical Ada Applications: A Critical Assessment, Proceedings of the 1996 Ada-Europe International Conference on Reliable Software Technologies, p.183-197, June 10-14, 1996

CITED BY 2

	P. N. Amey , B. J. Dobbing, Static analysis of Ravenscar programs, ACM SIGAda Ada Letters, v.XXIII n.4, p.58-64, December 2003
	V. Santhanam, The anatomy of an FAA-qualifiable Ada subset compiler, ACM SIGAda Ada Letters, v.XXIII n.1, p.40-43, March 2003