===========================================================================
CSC 236               Problem set 5                               Fall 2008
===========================================================================

(i) Consider the following program

--------
PS5(x)

# precondition" x is a natural number

  y= x*x
  while (y!=0) do {
    x = x -1
    y = y - 2*x - 1
  }
-------

Prove that PS5(x) halts whenever precondition holds.

Hint: Derive and prove a loop invriant whose purpose is to help prove 
termination.

(ii) What happens if we change the last line to
   y = y - 2*x
Will the program terminate? Prove or give an input that will 
lead to an infinite loop (you should prove that as well).

(iii) remember that a concatenation of two languages L and M (denote as
L o M is defined as 
      L o M = {xy | x in L, y in M}. 
For example if L is the language of all words consisting of the character a
and M is the language consisting of the chracter b then L o M is the 
language consisting of all strings that start with a's and end with b's.

Give an exmple of a language L such that 
      L = L o L