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 nindividual variables. EMLS sentences over n variables can be constructed from sentences in L4,2,n and L2,3,n, where Lk,m,n is the language of k relations of m arguments over n variables. We recursively define a match-counting algorithm for Lk,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 nw 2pnw - 1 (2 + k nm)). Match counting for Lk,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.