State Deltas: A Formalism for Representing Segments of Computation
Abstract
A state delta is a first-order predicate taking a precondition, a post-condition, a modification list and an environment list. State deltas are to be used in a proof system in which predicates describing the machine's current state are cross-referenced by the locations containing values used in each. Reasoning about a machine's forward progress may be carried out by successive application of state deltas. Application is legal if the precondition is true and if none of the locations in the environment list has been changed since the state delta was entered into the system. Afterward, all predicates cross-referenced to any of the locations in the modification list are deleted, and those in the post-condition list are added to form a new current state. If some locations hold arrays or lists, the cross-referencing part of the system may provide for attaching predicates to location components. If names may be given to individual location components, different predicates may depend upon the same values under different names. To keep track of all overlap conditions possible among a set of named locations, a graph structure with two node types is used to show all possible overlaps. A small proof system has been built and used to prove the correctness of a slice of the code in the ARPANET IMPs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1977
- Accession Number
- ADA046273
Entities
People
- Stephen D. Crocker
Organizations
- University of Southern California