Lecture notes on program inference rules [PDF] Summary of the PCA rules [PDF] Example program [PDF] Illustrated proof [PDF]