Given

var x;

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

Suppose we verify

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

We will reduce it to:

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

   assume Post(x);
   c2;
}

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

proc Q() {

 c1;
 dec();
 c2;

}