Position paper for the 21st Century Engineering Consortium Workshop

Beverly A. Sanders
Department of Comp. & Info. Sci. & Eng.
University of Florida
February 1998


In this  note, we  argue for  a deeper study of programming  than is
usually the case in the  introductory CS course.   By depth,  we mean
explicitly teaching   pragmatic techniques for  mathematical reasoning
about programs.  These  techniques are valuable  for all students, and
those who  later  study formal methods  can start  with  both a useful
foundation, as  well as a mind set  that being able to reasoning about
programs is a good thing.

The course described below has  been developed and taught at the University
of Florida  in the introductory  CS  course using  the Java programming
language  since  fall 1997.   A  textbook for the  course, written by the
author, is in progress.


Motivation

The  motivation for developing   a new introductory programming course was,
 in part, the  observation  (with teaching experience at  several
universities) that the   programming skills of many  advanced students are
hampered by  an inability to use  even very  simple mathematics in program
development.  A few examples should suffice to illustrate what is meant.


Consider the equation defining  the relationship between quotient  (/) and
remainder (%) operators in integer division.

   (x/y)*y + x%y == x

While this equation  can  often  be used  in  a quick  calculation  to
derive, simplify, or check  the correctness of  algorithms using / and %,
it never  occurs   to  most   students  to do  so.   Indeed,  most
introductory programming texts don't  even mention this  relationship, and
most students never learn it.


Another problem is the inability of  many students to  be able to deal with
 objects in programs that  aren't numbers.   A typical example of this is
the student who writes code such as

  if (x == 0) 
    done = true; 
  else 
    done = false;

instead of

  done = (x==0);

Along these same lines, some students who would have no problem with

     deposit(x + y + z)

where x,y,z  are numbers,  have  been  totally  confused by  a boolean
expression being used as a parameter in something like

     assert(x != 0);.

Although boolean expressions in the guards  of loops and if statements
present no problems, outside  of this  context, to  many students they are
unfamiliar and strange.

What makes this situation  so absurd is  that much of  the mathematics that
can  be  easily and  fruitfully applied in  programming is  quite
elementary compared to  the mathematics used  in other courses that we
require of   our   students.   What is    needed  is for   programming
mathematics to be explicitly taught.


Teaching programming for the 21st century

Taking as a given  that teaching elementary programming mathematics is a
desirable  goal, the questions remain  as  to exactly what  can and should
be taught.  The available introductory CS textbooks mostly fall into  one
of two  groups: those that  are completely non-mathematical; and those that
 equate   programming with formal  program  derivation, typically using a
language   specially designed for the   purpose, for which a compiler may
not even be available. The  lack of a compiler is viewed as an advantage as
it allows students to learn concepts without the  distraction of a machine.
 The former approach is inadequate, and regardless of the arguable
pedagogical merits  of the latter approach, political   and practical
realities  at  many  universities make it  anon-option.

In our course,  we strive to  find an appropriate and pragmatic middle
ground.  We  teach  object-oriented programming  using Java  augmented with
 explicit study of relevant  mathematics  and explanations of how this  can
be  used  in program development.   For the   most part, the mathematical
concepts that are  emphasized involve  understanding and using  the
properties  of   types   (rules for  manipulating  boolean expressions,
properties of string  concatenation, the equation (x/y)*y+ x%y == x for
int x,y, etc.) and using   assertions in a variety  of ways.  Assertions
appear  as documentation  (and  sometimes tests)  of program state at a
particular point in a program, constraints on input values, preconditions
and postconditions of  program  fragments  and methods, loop   invariants,
 class   invariants,  etc.    We    teach manipulation  and simplification
of  boolean  expressions, the  use of auxiliary variables, and the notions
of weaker and stronger.

Our treatment of loop invariants gives an idea of our approach.  We do not
emphasize developing  loop invariants from  a postcondition, which can be
quite  difficult.  Rather,  we   describe several  useful  loop idioms
along with  the loop  invariants  and variants  for the  idiom. Students
can recognize that a particular kind of loop has a particular kind of
invariant and variant, and use  the invariant to reason about the loop,
avoid off-by-one errors, avoid  non-termination, etc.  Since the sort of
loops  typically expected in  an  introductory course are fairly  simple,
this approach   works  well.  (Ideally, this  approach would also be
followed in the algorithms course.)

Benefits for formal methods

Clearly, the programming  mathematics   that we advocate  teaching  in
introductory computer science courses is not really ``formal methods''
although many of the concepts arise from  formal methods. In fact, our
treatment   is  often  decidedly  informal.    However, the underlying
message, that  programs  can  and should  be  subject  to mathematical
reasoning,  is the first  step  to an  appreciation of formal methods. Our
course should provide useful  skills to  all students, along with laying
the foundations for the future study of formal methods.