φj
slide: The correctness calculus