Here are some examples.
copy2
procedure copy2(x: integer class {x}; var y: integer class {x});   "copy x to y" var z: integer class {x}); begin z := 1; y := -1; while z = 1 do begin   y := y + 1;   if y = 0   then z := x   else z := 0 end end end copy2. |
Low < z Low < y z < y CIRCLEPLUS z y < y y < z x < z Low < z |
procedure copy2(x: integer class {x}; var y: integer class {x});   "copy x to y" var z: integer class {x}; begin 1: z := 1;   y := -1; 2: if z <> 1 then goto 6; 3: y := y + 1;   if y <> 0 then goto 5; 4: z := x;   goto 2; 5: z := 0;   goto 2; 6: end end copy2. |
b1 b2 b3 b4 b5 |
Department of Computer Science
University of California at Davis
Davis, CA 95616-8562