Inference Rules

for a

Simple Imperative Programming Language

 
 
 

Assignments	(x1,...,xn) := (e1,...,en)	{P[e]} x := e {P[x]}
Composition	[S;T]	{P}S{Q}   {Q}T{R} {P} [S;T] {R}
Conditional	if p then S else T	{P&p}S{R}   {P&~p}T{R}  {P}if p then S else T{R}
Loop	while p do S	{P&p}S{P}         {P}while p do S{P&~p}
Skip	skip	{P}skip{P}
Consequence		P -> Q   {Q}S{U}   U -> R  {P}S{R}