Experience with the formal semantic definition of HAL/S
Abstract
HAL/S is a large general purpose real-time programming language somewhat similar to ADA. Its major applications are for embedded real-time systems, in particular for the Space Shuttle on-board computer software and similar applications within NASA. After the language had been in regular use for several years, we were requested by NASA to prepare a formal semantic definition of the language using the method of H-graph semantics. This paper reports on the method and structure of that definition and on experience with its use in finding and correcting errors in the language specification and in the design of implementations for the language.
References
[1]
HAL/S Language Specification, Version IR-61-9, Intermetrics, Inc., Cambridge, MA, September 1976.
[2]
Pratt, T., "H-graph semantics, Part 1: Data structure grammars, Part 2: H-graph machines," DAMACS Reports 81-15 and 81-16, University of Virginia, September 1981, submitted for publication.
[3]
Pratt, T., "Application of formal grammars and automata to programming language definition," In Applied Computation Theory, R. T. Yeh, ed., Prentice-Hall, 1976.
[4]
Gordon, M., The Denotational Description of Programming Languages, Springer-Verlag, 1979.
[5]
Hoare, C. A. R., "An axiomatic basis for computer programming," Comm. ACM, Vol 12, No. 10, October 1969, 576-583.
[6]
Lucas, P. and Walk, K., "On the formal description of PL/I," Annual Review in Automatic Programming, 6, 3, Pergamon Press, 1969, 105-181.
[7]
Pratt, T. and Maydwell, G., "HAL/S formal semantic definition," SEAS Report UVA/528164/AMCS79/102, University of Virginia, August 1979, 350 pp.
[8]
Formal Definition of the ADA Programming Language, Honeywell, Inc., Cii Honeywell Bull, and Inria, November 1980 (preliminary).
[9]
Pratt, T. and Maydwell, G., "HAL/S language ambiguities and inconsistencies," SEAS Report UVA/528164/AMCS79/101, University of Virginia, July 1979.
[10]
Garman, J. R., personal communication, 1979.
[11]
Pratt, T., "HAL/S subset definition and implementation design for the NSSC-II flight computer," SEAS Report UVA/528164/AMCS79/103, University of Virginia, August 1979.
[12]
Maydwell, G., "Virtual computer to hardware mapping: an approach to programming language implementation," SEAS Report UVA/528164/AMCS79/104, University of Virginia, October 1979.
[13]
Feyock, S., "Formal semantic specifications as implementation blueprints for real-time programming languages," Proc. AIAA Computers in Aerospace Conf. III, Oct. 1981.
[14]
Gallant, S. "HAL/S language group memo no. 04-79," Intermetrics, Inc., May 22, 1979
[15]
Goos, G. and Wulf, W. "DIANA reference manual", Rept. CMU-CS-81-101, Dept. of Comp. Sci., Carnegie-Mellon Univ., March 1981.
Index Terms
- Experience with the formal semantic definition of HAL/S
Recommendations
Experience with the formal semantic definition of HAL/S
SIGPLAN '82: Proceedings of the 1982 SIGPLAN symposium on Compiler constructionHAL/S is a large general purpose real-time programming language somewhat similar to ADA. Its major applications are for embedded real-time systems, in particular for the Space Shuttle on-board computer software and similar applications within NASA. ...
Equivalence of formal semantics definition methods
AbstractThere are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 1982 Authors.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 June 1982
Published in SIGPLAN Volume 17, Issue 6
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 332Total Downloads
- Downloads (Last 12 months)63
- Downloads (Last 6 weeks)15
Reflects downloads up to 23 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in