| Summary: | 碩士 === 國立中山大學 === 應用數學研究所 === 83 === A good program should convince the users to apply its result to
solve their problem. To confirm the the correctness of a
program and to avoid applying the incorrect result given by
progam, program ver- ification is important for software
quality assur- ance(SQA). It can confirm that the output of the
program and the program specification are consist- ent. When
the program performs incorrectly, it also can help the
programmers to locate the faults of their program. This thesis
summarizes some techniques of prog- ram verification and
discusses the design and application of the verifier. A
verifier is a piece of a program that is embedded in the
program so that the program can perform self-checking during
its execution. By using the execution of verifier , the
programmer can confirm if the behaviour of the program segment
is correct or not. When design- ing the verifier of a program,
the completeness of input data, loop invariability of the
program and and complexity of verifier should be considered.
Some cases of verification are discusses in this thesis. The
problem of solving a system of linear equations "A x = b" and
the problem of sort- ing are presented as examples.
|
|---|
