The Modal Logic of Programs

Abstract

This document explores the general framework of Modal Logic and its applicability to program reasoning. The authors relate the basic concepts of Modal Logic to the programming environment: the concept of world corresponds to a program state, and the concept of accessibility relation corresponds to the relation of derivability between states during execution. The Temporal interpretation of Modal Logic is adopted. The variety of program properties expressible within the modal formalism is demonstrated. The first axiomatic system studied, the sometime system, is adequate for proving total correctness and 'eventuality' properties. However, it is inadequate for proving invariance properties. The stronger nexttime system obtained by adding the next operator is shown to be adequate for invariances as well. Additional keywords: computer logic.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1979
Accession Number
ADA155071

Entities

People

  • A. Pnueli
  • Z. Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Instructions
  • Invariance
  • Models
  • Numbers
  • Operating Systems
  • Prime Numbers
  • Real Numbers
  • Semantic Models
  • Sequences
  • Specifications
  • Structured Programming
  • Transitions

Readers

  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design