Formalizing the Analysis of Algorithms.
Abstract
Consider the average case analyses of particular deterministic algorithms. Typical arguments in this area can be divided into two phases. First, by using knowledge about what it means to execute a program, an analyst characterizes the probability distribution of the performance parameter of interest by means of some mathematical construct, often a recurrence relation. In the second phase, the solution of this recurrence is studied by purely mathematical techniques. The goal is to build a formal system in which the first phases of these arguments can be reduced to symbol manipulation. Formal systems currently exist in which one can reason about the correctness of programs by manipulating predicates that describe the state of the executing process. The construction and use of such systems belongs to the field of program verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1979
- Accession Number
- ADA086916
Entities
People
- Lyle Harold Ramshaw
Organizations
- Stanford University