Proofs of program correctness tend to be long and tedious whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In addition to simplifying certification of correctness, this method simplifies the process of providing specifications for a program. The applicability of this technique to procedures, recursive programs, and modular programs is demonstrated.

It is shown that there is a sequence of languages E1, E2,... such that every correct prefix parser (one which detects errors at the earliest possible moment, e.g., LR or LL parsers) for En has size 2cn, yet a deterministic PDA recognizing En exists and has size O(n2). There is another easily described sequence of languages N1,N2,... for which Nn has a nondeterministic PDA of size O(n2) but no deterministic PDA of size less than 2cn. It is shown moreover, that this latter exponential gap can be made arbitrarily large for different sequences of languages.

Recently strict deterministic grammars and languages have been introduced [9,10,11]. This family of languages is quite fundamental in the study of the mathematical properties of deterministic languages and in dealing with some classical families of grammars such as LR(k) and bounded right context grammars [7,8,14]. These grammars are closely related to LR(0) grammars [1,12,13,14], in fact each strict deterministic grammar is also LR(0). In the present paper, we consider the question of how to parse strict deterministic grammars. We introduce part of a more general theory called "characteristic LR(k) parsing". This actually produces parsers which are tuned to the characteristics of a particular family of grammars. We apply the theory to the family of strict deterministic grammars and we get parsers which are as fast as canonical LR(k) parsers but are substantially smaller. They are not necessarily minimal but we postpone any discussion of minimality to the sequel.The techniques used in the present discussion are quite general [5]. For instance, the study in [3] is similar in spirit to our technique. The optimization techniques for LR(k) parsers in [2] do not work in the case k = 0 without modification. After modifying those methods for k = 0, it can be shown that our parsers cannot be produced by those techniques. This fact has its positive aspect in that our parsers may be smaller and its negative aspect in that error detection may be delayed.The present paper is divided into the present introduction and three sections. In the remainder of this introduction, some basic definitions of strict deterministic and LR(k) parsing are given. We have tried to follow [1] as much as possible in order to minimize the amount of new material to be absorbed. The order of the results is the order needed to prove that the characteristic parser works. In Section III, we apply the theory of Section II to strict deterministic parsing. A simple example shows that the new parsers can be unboundedly smaller than the canonical LR(0) parser.The present paper is meant to be an extended abstract and no proofs are included.The rest of the introduction is concerned with notational conventions for the technical concepts needed.