A. Vargun (USA)
Termination, Code-Carrying Theory, Correctness, Verifica tion
One approach to mechanizing proofs of termination is to require that each new recursive function definition be ac companied by an ordering relation. The main disadvan tage of this methodology is to determine an ordering rela tion first and prove the termination based on it. This paper describes an alternative approach that does not require a separate order relation. The proof of termination is con structed as a proof by induction that mirrors the recursion structure in the axioms. We generate for each new func tion being defined a termination condition (TC), and from each axiom of the function’s definition we generate a cor responding termination axiom. Using the resulting set of termination axioms, we construct a proof of the TC. Both TC and termination axioms are generated automatically by applying a simple tool called TCGEN. If the termination is proved, another tool called CODEGEN can be applied to the axioms to construct a recursive function.
Important Links:
Go Back
