tedious tasks. Experiments showed that instead of buggy programs, programmers
wrote buggy logic specifications and buggy program proofs.
Van der Linden [ 2 , p. 287], gives some examples of complicated proofs that are
much harder to verify than the programs they are trying to prove.
Program proof techniques are valuable for proving the correctness of individual
methods that make computations in nonobvious ways. At this time, though, there
is no hope to prove any but the most trivial programs correct in such a way that the
specification and the proof can be trusted more than the program. There is hope
that correctness proofs will become more applicable to real-life programming
situations in the future. However, engineering and management are at least as
important as mathematics and logic for the successful completion of large software
6.6 Using a Debugger
As you have undoubtedly realized by now, computer programs rarely run perfectly
the first time. At times, it can be quite frustrating to find the bugs. Of course, you can
insert print commands, run the program, and try to analyze the printout. If the printout
does not clearly point to the problem, you may need to add and remove print
commands and run the program again. That can be a time-consuming process.
Modern development environments contain special programs, called debuggers, that
help you locate bugs by letting you follow the execution of a program. You can stop
and restart your program and see the contents of variables whenever your program is
temporarily stopped. At each stop, you have the choice of what variables to inspect
and how many program steps to run until the next stop.
A debugger is a program that you can use to execute another program and analyze
its run-time behavior.
Some people feel that debuggers are just a tool to make programmers lazy.
Admittedly some people write sloppy programs and then fix them up with a
debugger, but the majority of programmers make an honest effort to write the best
program they can before trying to run it through a debugger. These programmers