Evaluation of verifiability in HAL/SThe ability of HAL/S to write verifiable programs, a characteristic which is highly desirable in aerospace applications, is lacking since many of the features of HAL/S do not lend themselves to existing verification techniques. The methods of language evaluation are described along with the means in which language features are evaluated for verifiability. These methods are applied in this study to various features of HAL/S to identify specific areas in which the language fails with respect to verifiability. Some conclusions are drawn for the design of programming languages for aerospace applications and ongoing work to identify a verifiable subset of HAL/S is described.
Document ID
19790070414
Acquisition Source
Legacy CDMS
Document Type
Conference Proceedings
Authors
Young, W. D. (Texas Univ. Austin, TX, United States)
Tripathi, A. R. (Texas Univ. Austin, TX, United States)
Good, D. I. (Texas Univ. Austin, TX, United States)
Browne, J. C. (Texas, University Austin, Tex., United States)