CIS 425 Homework III

Loops; due 10/19

Part I

You are given a collection of datatypes that represent the core of a typical imperative language (essentially the grammar of Figure 3.3 but with minor variations):


datatype Bop = Plus | Minus | Mult | Div | Equal | Less | Greater | And | Or

datatype stat = 
    Assign of string * exp  
  | Sequence of stat list          
  | Ifthen of exp * stat
  | Ifthenelse of exp * stat * stat
  | While of exp * stat
  | Repeat of stat list * exp
  | Forup of string * exp * exp * stat
  | Fordown of string * exp * exp * stat
  | Case of exp * (int * stat) list

and exp = 
    Var of string
  | Number of int
  | Boolean of bool
  | Binary of exp * Bop * exp 
  | Not of exp

Write an ML function that accepts an arbitrary stat and eliminates from it all occurrences of

 Repeat, Forup, Fordown,

and Case . For example,

 
- ... in SML ...
(* so we can see the output clearly *)
- Compiler.Control.Print.printDepth := 100;
- Compiler.Control.Print.printLength := 1000;

- expandstat (Repeat([Assign("x",Number(3)), Assign("z",Number(4))], Var("y")));
val it =
  Sequence
    [Assign ("x",Number 3), Assign ("z",Number 4),
     While (Not (Var "y"),
            Sequence [Assign ("x",Number 3),Assign ("z",Number 4)])]
  : stat
(* 
converted
  repeat x=3; z=4; until y 
to 
  x =3; z=4;
  while (not y) do x=3; z=4;
*)

- expandstat(Case(Var("x"), [(0,Assign("y0",Number(10))), (1,Assign("y1",Number(11))), (2,Assign("y2",Number(12)))]));
val it =
  Sequence
    [Assign ("temp",Var "x"),
     Ifthenelse
       (Binary (Var "temp",Equal,Number 0),Assign ("y0",Number 10),
        Ifthenelse
          (Binary (Var "temp",Equal,Number 1),Assign ("y1",Number 11),
           Ifthen
             (Binary (Var "temp",Equal,Number 2),Assign ("y2",Number 12))))]
  : stat
(*
converted
  case x of 
    0: y0 = 10;
    1: y1 = 11;
    2: y2 = 12;
to 
  temp = x
  if temp=0 then y0=10
  else if temp=1 then y1=11
  else if temp=2 then y2=12
*)


- expandstat (Forup("x",Number(0),Number(10),Assign("y",Number(100))));
val it =
  Sequence
    [Assign ("x",Number 0),
     While
       (Not (Binary (Var "x",Greater,Number 10)),
        Sequence
          [Assign ("y",Number 100),
           Assign ("x",Binary (Var "x",Plus,Number 1))])] : stat
(* converted
  for x = 0 upto 10 do y=100
to 
  x = 0;
  while (not (x > 10)) do y = 100; x = x+1; 
*)

Part II

Let P be the predicate { x >= 0 AND y > 5 } .
Let Q be the predicate { x >= 0 AND y <= 5 } .
Prove that if P holds before the following loop:

repeat 
  x = x + y; 
  y = y - 1; 
until y <= 5

then Q will hold after the loop.

Visited

times since September 21, 1999 (or the last crash).

sabry@cs.uoregon.edu