Given

var x, y;

proc P() 
requires Pre(x,y)
ensures Post(x,y)
{ c }

Suppose we verify

proc Q() {
   c1;
   P();
   c2;
}

We will reduce it to:

proc Q() {
   c1;
   assert Pre(x,y);

   assume Post(x,y);
   c2;
}

var x : int;

proc dec()
requires x > 0
ensures x <= (old x)
{ x = x - 2; }

proc Q()
{
   c1;
   dec();
   c2;
}

One way to derive rules: use assignments to reduce parameters to changes to global state.