The Gist Behavior Explainer.
Abstract
One difficulty in understanding formal specifications is that there are often interactions between pieces of the specification, never explicitly stated, that only become apparent when the specification is analyzed or simulated. Symbolic evaluation has been proposed as a way of making such interactions apparent, but symbolic evaluators often produce enormous execution traces that are tedious and difficult to examine. This paper presents an automated system that employs a number of heuristics to select the most interesting aspects of the trace for presentation. The system uses this information to construct an English description of the trace. Due to the need for summarization and proof reformulation, the direct-translation approach, which worked well in describing specifications statically, is not suitable in this case. This paper describes the system and gives an example of its output. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1983
- Accession Number
- ADA130730
Entities
People
- William R. Swartout
Organizations
- University of Southern California