procedure a, b, c := P(x, y, z)
  requires 10
  ensures 20
do
  if 30 then else end;
  if 31 then else end;
  while x < z
    invariant x <= z
    invariant b.valid and 1
  do
    k := x + 1;
  end;
  (x+5).head := c.tail;
  a := new (17, 18);
  assert a != null;
  m := k + a + null;
  c := m;
  call Q(x, y, y);
  if x then
    call a, c, b := P(a, b, c);
  else
    call R();
  end;
end;


procedure Q(x, y, z)
  requires 10
  ensures 20
do
  if 40 then else end;
end;


procedure R()
  requires 10
  ensures 20
do
end;