Formal method of procedure call based on Hoare logic
Zhang Lai-shun · Jisuanji gongcheng yu sheji · 2011
Techniques and algorithms for deriving specifications directly from code for procedures and for deriving specifications of the semantic effects of calling those procedures are presented based on Hoare logic style reasoning.In order to reason about the semantic effects of a procedure call,the semantic specification of the procedure is called as an independent abstract unit needs to be abstracted.A specific procedure call is given,and the formal precondition is abstracted that hold at invocation of a procedure,and then these conditions is used as a precondition to the procedure body to calculate its strongest postcondition,the postcondition is also the semantic effects of procedure call.