Accession Number:

ADA275852

Title:

Reasoning About Programs by Exploiting the Environment

Descriptive Note:

Interim rept.

Corporate Author:

CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1994-02-02

Pagination or Media Count:

44.0

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 programs 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.

Subject Categories:

  • Psychology
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE