COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro.tex[tur,cjs]
C00003 00003	\sect{STAN-CS-80-804 (AIM-336)}
C00006 00004	% ∞∞∞∞∞∞∞∞∞
C00012 ENDMK
C⊗;
\input macro.tex[tur,cjs]

\vfill
\endpartx
\sect{STAN-CS-80-804 (AIM-336)}

{\ic Determining Correctness by Testing}
by Martin Brooks (Thesis, 135 pages, May 1980)

This report presents a mathematical theory of program testing which
describes how testing can be used to show a program's correctness.
We study the situation where
the programmer
has written a program P which is either correct or which differs
from the correct program by one or more errors in a specified class E.
The theory relates:

\bite The combinatorics of how errors in E could have led to P being written.

\bite The type of program behavior that the programmer will observe when testing; for
example the program's output or a trace.

\bite The characteristics of test data which is guaranteed to reveal
the presence of errors in P.

The theory is developed at a general level and is then specialized
to the case of recursive programs having only certain types of simple errors, where the
programmer observes a trace of each test run. 
We derive a method for generating test data for recursive programs.
The generated test data is %2complete%1,
meaning that if the only errors in the recursive program are of the specified simple types,
then the test data will
reveal the errors through at least one incorrect trace. Viewed contrapositively,
if one assumes that the program differs from
the correct program at most by errors of the specified simple types,
then if the trace of each
test run is as the programmer intended, then the program must be correct.
The test data generation method has been implemented and examples
of its operation are given.

% ∞∞∞∞∞∞∞∞∞
\vfill\end
% ∞∞∞∞∞∞∞∞∞