|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6191
| Title: | Reasoning About Programs by Exploiting the Environment |
| Authors: | Fix, Limor
Schneider, Fred B. |
| Keywords: | computer science
technical report |
| Issue Date: | Feb-1994 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR94-1409 |
| 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 by (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. |
| URI: | http://hdl.handle.net/1813/6191 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
