Com S 641 Semantic Models for Programming Languages
			     Homework: 6

E. Cohen.  Programming in the 1990s. Springer-Verlag, 1990.  Chapters 8,9

The aim of this homework is to further develop your skills at calculating
programs, by giving you some practice with loops.  This completes the
motivational and background section of the course.  (Buy the Hesselink book
now if you haven't already.)

(Chapter 8)
This chapter is really an introduction to chapter 9.
Focus on the steps in developing a loop.  Note that chapter 9 is only one
of two heuristics for developing loops.  Chapter 10, which we won't cover,
develops another.
a. Which steps in the development of a loop involve creativity and experience?
   Which steps are just straightforward calculation?

(Chapter 9)
This chapter focuses on one strategy for finding an invariant:
deleting a conjunct from the postcondition desired.
b. (Cohen's 9.1)  Try solving the problem of integer division,
   choosing as the invariant the following:
	P: r < y /\ q*y+r = x
   You will run into trouble.  Where do you run into trouble and why?
c. (extra credit) do Cohen's 9.0.
d. (Cohen's 9.2)  Given functions G and H, point x is a "crossing point"
   when G.x = H.x.  Given that there is a crossing point, determine the
   smallest natural number that is a crossing point.  (Apply linear search.)
e. (Cohen's 9.4)  The number of rabbits at ISU in month x >= 0 is given by R.x.
   The rabbit population is stable at month x when R.(x+1) = R.x.
   Given that the rabbits are stable in some month, determine the first such
   month.  (Imagine we have an array of data in R.  Apply linear search.)
f. (extra credit) Do one of Cohen's exercises 9.3 or 9.5.
g. (extra credit) If linear search has billions and billions of uses,
   is the right thing to do to teach thousands and thousands of programmers
   to just recognize it and write it correctly millions of times?
h. (Cohen's exercise 9.7) Develop a different solution for S0
   (the choice of a d to satisfy 1 <= d /\ d * y <= r on page 145).
   Arrive at a different invariant by deleting the conjunct R1 from RR.
   Division of a power of 2 by a power of 2 is allowed (i.e., shifting right),
   but exponentiation is not.

(Cohen's chapters 10 - 13)
We won't be using this part of the book.  However, if you wish to do
any exercises from this part of the book, seriously, I'm willing to
give you feedback on them.

You might want to skim the rest of the book.  Take a look at chapter
13 for a summary and some pointers to the literature.