execution satisfies the postcondition. Notice that the definitions of weakest-precondition given above (in particular for while-loop) preserve this property. Selection Selection is a generalization of if statement: Here, when two guards and are simultaneously true, then execution of this statement can run any of the associated statement or . Repetition Repetition is a generalization of while statement in a similar way. Specification statement Refinement calculus extends GCL with the notion of specification statement. Syntactically, we prefer to write a specification statement as which specifies a computation that starts in a state satisfying pre and is guaranteed to end in a state satisfying post by changing only x. We call a logical constant employed to aid in a specification. For example, we can specify a computation that increment x by 1 as Another example is a computation of a square root of an integer. The specification statement appears like a primitive in the sense that it does not contain other statements. However, it is very expressive, as pre and post are arbitrary predicates. Its weakest precondition is as follows. It combines Morgan's syntactic idea with the sharpness idea by Bijlsma, Matthews and Wiltink. The very advantage of this is its capability of defining wp of goto L and other jump statements. Goto statement Formalization of jump statements like goto L takes a very long bumpy process. A common belief seems to indicate the goto statement could only be argued operationally. This is probably due to a failure to recognize that goto L is actually miraculous (i.e. non-strict) and does not follow Dijkstra's coined Law of Miracle Excluded, as stood in itself. But it enjoys an extremely simple operational view from the weakest precondition perspective, which was unexpected. We define For goto L execution transfers control to label L at which the weakest precondition has to hold. The way that wpL is referred to in the rule should not be taken as a big surprise. It is just wp(L:S, Q ) for some Q computed to that point. This is like any wp rules, using constituent statements to give wp definitions, even though goto L appears a primitive. The rule does not require the uniqueness for locations where wpL holds within a program, so theoretically it allows the same label to appear in multiple locations as long as the weakest precondition at each location is the same wpL. The goto statement can