{ INV and k < b } loop_body { INV }
{ PRE } k := a { INV }
show { INV' } k := a { INV } and PRE ==> INV'
INV and ~(k < b) ==> POST
{ PRE } program { POST }