Partial Correctness Step

A portion of proof in Program Correctness $(\text{precondition and termination})⟹\text{postcondition}$