LARA This is an old revision of the document! Assume Guarantee Reasoning with Procedures Procedures without parameters or results Given 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); havoc x; assume Post(x); c2; } Handling Parameters