| << Chapter < Page | Chapter >> Page > |
For instance, in the first board, what assertions can we be sure of? What, exactly, is your reasoning?How about in the second board? You can certainly envision wanting a computer player thatcan deduce certain moves, an make those for you automatically.
When writing a program, we'd like to simply look at the program and
determine whether it has any bugs, without having to run it.We'll see in the future, however, that such a general problem cannot be
solved. Instead, we focus on finding more limited kinds of errors.
Type checking determines whether
all functions are called with the correct
type of inputs.
+ should be
called with numbers, not Booleans,and a function which a programmer has declared
to return an integer really should always return an integer.Consider the following program:
// average:
// Simply divide sum by N, but guard against dividing by 0.//
real-or-false average( real sum, natNum N ) {if (N != 0)
return sum / N;else
return false;}
One reason programmers are required to declare the intended
type of each variableis so that the computer (the compiler) can
prove that
certain errors won't occur.How can you or the compiler prove, in the above,
that
average returns a real number or false,
but never returns (say) a string, and doesn't raise an exception?Deductions are made based on premises about the types that are passed in,
along with axioms about the input and return types of the built-in functions
if ,
!= , and
/ ,
as well as which exceptions those built-ins might raise.
Consider this variant:
// augment-average:// Given an old sum and N, compute the average if one more
// datum were included.//
real augment_average( real old_sum, natNum old_N, real new_datum ) {return average( old_sum + new_datum, old_N + 1 );
}
Most compilers will reject
augment-average , claiming
that it may actually return
false .
However, we're able prove that it really willonly return a
real ,
by using some knowledge about natural numbers and adding 1,plus some knowledge of what
average returns.
(Note that our reasoning uses aspects of
average 's interface which aren't explicitly stated;
most type systems aren't expressive enough to allow more detailed type contracts,
for reasons we'll allude to later.)So we see that many compilers have overly conservative type-checkers,
rejecting code which is perfectly safe,because they are reasoning with only a narrow set of type-rules.
This example alludes to another use of logic: Not only is it the foundation of writing proofs(ones that can be created or checked by computers), but logic can also be used asan unambiguous specification language . Observe that while a function's implementation is always specifiedformally and unambiguouslyin a programming languagethe interface is specified entirely English, aside from a few type declarations.Many bugs stem from ambiguities in the English, that different humans interpret differently (or, don't think about).Being able to use logic to specify an interface (and cannot be modified even if the somebody later tunes the implementation)is an important skill for programmers, even when those logic formulas aren't used in proofs.
Given a circuit's blueprints, will it work as advertised? In 1994, Intel had to recallfive million of its Pentium processors, due to a bug in the arithmetic circuitry : This cost Intel nearly half a billion dollars, lots of bad publicity , and it happened after intensive testing. Might it have been possible to have a program try to prove the chip's correctness or uncover an error, before castingit in silicon?
Software and hardware companies are increasingly turning to the use of automated proofs, rather than semi-haphazard testing,to verify (parts of) large products correct. However, it is a formidable task,and how to do this is also an active area of research.
There are of course many more examples; one topical popular concern is verifying certainsecurity properties of electronic voting machines (often provided by vendors who keep theirsource software a proprietary secret).
Having proofs of correctness is not just comforting; it allows us to save effort (less time testing,and also able to make better optimizations), and prevent recall of faulty products.But: who decides a proof is correctthe employee with best SAT scores?!? Is there some trusted way to verify proofs,besides careful inspection by a skilled, yet still error-prone, professional?
Many highly intelligent people are poor thinkers. Many people of average intelligence are skilled thinkers.The power of the car is separate from the way the car is driven.Edward De Bono, consultant, writer, and speaker (1933- )
Notification Switch
Would you like to follow the 'Intro to logic' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|