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 |
Send email to
cs253@csif.cs.ucdavis.edu.
Department of Computer Science
University of California at Davis
Davis, CA 95616-8562