Operation decomposition proof obligations for blocks and procedures. - Jean Alain Ah-Kee (1989)