An Approach to Automated Reasoning About Operational Semantics.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1994
Accession Number
ADA291127

Entities

People

  • A. Cant
  • M. A. Ozols

Organizations

  • Defence Science and Technology Group

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Australia
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Electronics
  • Language
  • Programming Languages
  • Set Theory
  • Software Development
  • Specifications
  • Systems Engineering
  • Translations
  • User Interface
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Artificial Intelligence
  • Cybersecurity.
  • Software Engineering.