Reasoning About Programs by Exploiting the Environment

Abstract

A method for making aspects of a computational model explicit in the formulas of a programming logic is given. The method is based on a new notion of environment--an environment augments the state transitions defined by a program's atomic actions rather than being interleaved with them. Two simple semantic principles are presented for extending a programming logic in order to reason about executions feasible in various environments. The approach is illustrated (i) discussing a new way to reason in TLA and Hoare-style programming logics about real-time and by (ii) deriving the first TLA and Hoare- style proof rules for reasoning about schedulers.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 02, 1994
Accession Number
ADA275852

Entities

People

  • Fred B. Schneider
  • Limor Fix

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Language
  • Materials
  • Military Research
  • New York
  • Operating Systems
  • Programming Languages
  • Reasoning
  • Security
  • Software Development
  • Transitions
  • Universities

Fields of Study

  • Computer science

Readers

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