More on Compositionality (Tr,g)(S,R,G) (T2,g)S(S2,R,G) (T T2,,g)s(SS,,R, G) (T,r, ss,,g) b<→B (while b do t, g s while b do s,R,g An axiomatic proof system for refinementMore on Compositionality (T1 , r, g) ≲ (S1 , R, G) (T2 , r, g) ≲ (S2 , R, G) (T1 ; T2 , r, g) ≲ (S1 ; S2 , R, G) (T, r, g) ≲ (S, R, G) b  B (while b do T, r, g) ≲ (while B do S, R, G) An axiomatic proof system for refinement …