DEPARTMENT OF COMPUTER SCIENCE

DOCTORAL DISSERTATION DEFENSE

Candidate: Lars Ericson

Advisor: Bhubaneswar Mishra

Title:*Gedanken*: A tool for pondering the

tractability of correct program technology

3:00 p.m., Thursday, March 31, 1994

rm. 402, Warren Weaver Hall

DOCTORAL DISSERTATION DEFENSE

Candidate: Lars Ericson

Advisor: Bhubaneswar Mishra

Title:

tractability of correct program technology

3:00 p.m., Thursday, March 31, 1994

rm. 402, Warren Weaver Hall

Abstract

We examine the feasibility of the Correct Program Technology (CPT) approach to program verification using available technology, with pessimistic results.

We compare CPT with RAPTS and the Calculus of Constructions. We specify the Correct Programmer's Workbench (CPW), and review six programming environments as platforms. We define a Correct Program Editor and prototype it in Mathematica.

CPT applies decision procedures for specification sublanguages to make shorter proofs, hoping these shorter proofs will have faster verifications, but these sublanguages are NP-Complete or worse. We review some heuristics for improving their average case. CPT relies on a sublanguage of set theory, MLS. We prove that MLS is NP-average complete in the sense of the Levin-Gurevich theory of average case complexity. We conjecture that shorter proofs of random theorems cost more to verify.

EMLS is an elementary relational language (ERL). We define syntactic
simplification rule sets (SSRs) for ERLs. The average case effect of an SSR is
determined by the number of matches of the SSR with ERL sentences of *n*individual variables. EMLS sentences over *n* variables can be constructed from
sentences in *L*_{4,2,n} and *L*_{2,3,n}, where *L*_{k,m,n} is the language of
*k* relations of *m* arguments over *n* variables. We recursively define a
match-counting algorithm for *L*_{k,m,n} SSRs and extend it to EMLS. If an SSR
has *p* patterns in *w* pattern variables over *n* individual variables, match
counting costs
*O*(*p n*^{w} 2^{pnw - 1} (2 + *k n*^{m})). Match counting for
*L*_{k,0,0} is in #P, and we conjecture that it is #*P*-Complete. We
conjecture generating functions do not yield a method of approximating the
number of matches, and we conjecture that the problem of approximating matches
is also #*P*-Complete. We count the matches for low *n* for some EMLS SSRs,
with discouraging results, and note that the matches of an effective rule set
must grow as the size of the language for *n* variables.

We conclude that the remaining hope for verification is to build a large library of specification language constructs which occur frequently and can be verified in polynomial time.