Sequential Composition
A way of composing larger programs from smaller segments
If s1 and S2 are commands then s1;s2 is a new command
wp (s1;s2, R) = wp(s1, wp(s2, R))
x is a simple variable, e is an expression and the types of x and e are the same
wp(x := e, R) = domain(e) cand Rex
Domain(e) is a predicate that describes the set of all states in which e may be evaluated i.e. is well defined.
Usually we write: wp(x := e, R) = Rex