The rule of composition captures the elementary sequential composition of programs. As premises, we have two assumptions about the partial correctness of two programs α1 and α2. The first assumption is that when α1 is executed in a state satisfying A, then it will finish in a state satisfying B, whenever it halts. The second assumption is that when α2 is executed in a state satisfying B, then it will finish in a state satisfying C, whenever it halts. The conclusion of the rule is about the partial correctness of the program α1;α2 (i.e., α1 sequentially composed with α2), that follows from the two assumptions. Namely, we can conclude that if α1;α2 is executed in a state satisfying A, then it finishes in a state satisfying C, whenever it halts. 