Accession Number : ADA291127

Title :   An Approach to Automated Reasoning About Operational Semantics.

Descriptive Note : Research rept.,

Corporate Author : DEFENCE SCIENCE AND TECHNOLOGY ORGANIZATION CANBERRA (AUSTRALIA)

Personal Author(s) : Cant, A. ; Ozols, M. A.

PDF Url : ADA291127

Report Date : AUG 1994

Pagination or Media Count : 58

Abstract : The assurance of the safety or security of critical software rests on a clear understanding of the formal semantics of the programming language used. Operational semantics is the most widely used means of formally defining a language. The need for high levels of assurance, along with the complexity of these definitions for real programming languages, means that tool support is essential for carrying out reasoning about code with respect to the language definition. In this paper, we describe a generic approach to automated reasoning about the operational semantics of programming languages. As an application of this approach, we describe the construction of an environment for reasoning about programs written in a functional subset of ML. The system we describe (called Elle) captures the formal operational semantics definition of a large subset of Standard ML within the theorem prover Isabelle, and provides some support for the verification of ML programs. (AN)

Descriptors :   *PROGRAMMING LANGUAGES, *COMPUTER PROGRAM VERIFICATION, SOFTWARE ENGINEERING, REQUIREMENTS, AUTOMATION, DATA PROCESSING SECURITY, COMPARISON, REASONING, COMPUTER LOGIC, SEMANTICS, OPERATING SYSTEMS(COMPUTERS), AUSTRALIA, CONTROL SEQUENCES.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE