Thanks to Dean Herington for the derivation.
Consider a `repeat loop' construct: repeat S until B Its inference rule as derived by the "flowchart" method is: { P } S { Q }, (Q and ~B) ==> P ---------------------------------- { P } repeat S until B { Q and B } Let's derive the same inference rule by defining the repeat loop construct to be equivalent to: S; while ~B do S 1. { P } S { Q } assume 2. (Q and ~B) ==> P assume 3. { Q and ~B } S { Q } restrict the precondition of 1 using 2 4. { Q } while ~B do S { Q and B } apply `while' rule to 3 5. { P } S; while ~B do S { Q and B } compose 1 and 4 6. { P } repeat S until B { Q and B } recast 5 using definition of `repeat' Thus, given 1 and 2 we may conclude 6.