Lab 10
Introduction to C

Comp 210

Spring 1996

Contents

Induction

Induction is a technique, demonstrated in the last two lectures, for proving infinitely many propositions at once. For instance, recall the definition

displaymath115

Suppose that we want to prove the claim

displaymath117

That represents infinitely many equations, including the following:

eqnarray13

Each of these equations is easy enough to prove on its own, but it would seem that proving infinitely many equations takes infinitely many proofs.

Induction is a technique for using just two short proofs to prove infinitely many facts. There are two key parts to an inductive proof:

the base case
is a proof of one concrete small case; you just work out by hand that the property you care about holds.
the inductive step
shows how to extend a proof; in other words, given a proof, the inductive step transforms the proof into a new proof that proves the property for a different value

An example

Let's do an example. For the base case we choose a small value--say, 1. The proof is quite easy (the sequence of values from 1 to 1 consists of just the value 1):

eqnarray26

On the other hand, it would be quite tedious to prove

eqnarray37

This would require quite a bit of math.

However, suppose that you were permitted to assume that

eqnarray47

Then proving the property would be easy again:

eqnarray57

If we already have a proof that does most of the work for us, then extending that proof to demonstrate a new equation is not hard. We can generalize the above proof to show how, given a proof for arbitrary n, we can extend it to n+1:

eqnarray77

The inductive principle

Now we have a new technique for proving the equations for any value of n: we start with the base case and repeatedly apply the inductive step until we have a proof for the desired value of n. For instance, to prove the equation for n=3, we start with the base case (n=1) and then apply the inductive step twice: once to demonstrate the equation for n=2, and once to extend it to n=3. Similaraly, the proof for n=527 consists of the base case plus 526 applications of the inductive step.

The inductive principle states that if we have a proof for the base case and a technique for extending a proof to the next logical step (in this case, extending a proof for one number to the next greater number), then we can construct a proof for any value at all. In other words, two small proofs--for the base case and the inductive step--were able to replace arbitrarily many proofs, one for each value of n. We have succeeded in proving our equation for every value of n.

Why do we care?

After writing a program, you must verify that it is correct. (An incorrect program is in some ways worse than no program at all.) So far we have used testing to confirm that our programs operate correctly, but testing can only prove negative facts, not positive ones. That is, testing can demonstrate that a program is incorrect by giving an input for which the program gives the wrong answer, but testing cannot show that a program is correct for all inputs, because there might be some input for which the program fails (but which you forgot to test).

While testing produces facts about individual inputs, induction can make statements about groups of inputs, or about every possible input. Thus, induction is a technique for proving programs correct and providing complete confidence in your code, while testing can at best only provide partial confidence (unless you test your code on every possible input, which is generally an impossible task).

Induction is the natural counterpart to recursion: when you have created an arbitrarily-large object (or sequence of calls) via recursion, the best way to reason about it is via induction. The induction base case deals with the recursion base case, and the inductive step deals with the recursion.

Emacs

Emacs supports a number of features that make editing and running C programs very convenient, so we will use the Emacs editor for the rest of the term. Many of you are already familiar with Emacs; here is some review that all of you might find helpful.

Start up Emacs by typing gnuemacs at your shell prompt or using the mouse to get the ``Comp 210 tools'' menu. Emacs is an editor, but it is also a richly-featured program development environment and much, much more. Many people, including the instructor for this course, do all their work from Emacs, including filesystem traversal, editing, reading and sending news and mail, debugging, surfing the Web, etc.

Emacs manages a collection of buffers, some of which are visible on the screen and some which may be hidden. A buffer is the object holding the text from a file or some other information, such as interaction with a program being run from Emacs. The blank line below the reverse-video status line is called the echo area (when Emacs uses it to display messages) or the the minibuffer (when you use it for specifying complex commands). Most Emacs commands have a long form starting with M-x and a short keystroke sequence (a keyboard accelerator). For instance, you can edit a file in its own buffer by doing any of

M-x find-file RET
type M-x, then type "find-file", then finally press the return key
C-x C-f
C-x is control-x: hold down the control key, press and release x, let up on the control key
via the mouse
select the "Open File..." item from the "Files" pull-down menu

and then type the filename and press the return key.

M-x is the meta-x keystroke, which you type by holding down the meta key (the diamond next to the space bar), pressing and releasing x, then letting up on the meta key. On some machines lacking a meta key, the alt key works as a meta key. If you don't have an alt key (or it doesn't work as a meta key), then you can type ESC x instead (press and release the escape key, then press and release x).

The universal quit command in Emacs is C-g; it almost always aborts the current command. Frequently, pressing ESC three times will also abort the current comment and/or quit the current mode.

Emacs is extensively documented; it is very easy to get help or to learn more about it. The keystroke C-h invokes help in Emacs; you follow it by another key to indicate what kind of help you want. To learn more about what sorts of things you can type after the first C-h, type a second one: C-h C-h. Some particularly useful help keystrokes are:

C-h t
run an Emacs tutorial
C-h i
invoke the Info documentation system
C-h m
get documentation on the current mode (such as C++ mode)
C-h a
get a list of commands relating to a word you type ("apropos")

Of course, you can just use the pull-down menus if you prefer; most of Emacs's functionality is available from them. The place to start looking for help is on the "Help" menu.

The tutorial directory, ~comp210/Labs/lab10/, contains a copy of the quick reference card for Emacs; it was also handed out in lab.

You might want to learn about multiple windows in Emacs, switching among windows and buffers, incremental searching, marking regions, the Dired directory editor, indenting C/C++ code, spell-checking, Emacs's command and filename completion facilities, and command shells within Emacs.

Compiling C++ programs

You are strongly encouraged to read the Extended C Primer that was handed out in class and is available on the WWW. It introduces you to the C language, and we will assume that you understand the material presented there. (So far you should have read up to, but not including, the section on arrays.)

Copy the contents of the lab directory by executing the following commands from a Unix shell:

  cp -r ~comp210/Labs/lab10 ~/comp210
  cd ~/comp210/lab10
Use Emacs to view the file simple.cc, which contains the following text:
// An example program in Extended C
// Compile via g++ -Wall -g -o simple simple.cc

#include <iostream.h>

int Fact(int n)
{
  if (n == 0)
    return 1;
  else 
    return n * Fact(n-1);
}

int main()
{
  int n;
  cout << "Enter a natural number ";
  cin >> n;
  cout << n << " factorial is " << Fact(n) << "\n";
}

Quota

If you run out of quota while compiling programs, use du to find out where space is being taken up. Likely possibilities include old executables and your Netscape cache.