A method for generating program specification from source program - analysis by transforming program structure and argument manipulation. - Takahiro Nagai; Takeshi Imanaka; Jun'ichi Toyoda; Tsukasa Hirashima; Kuniaki Uehara; Yuichi Nagasawa (Syst. Comput. Jpn., 1995)