Automatic termination analysers typically measure the size of terms applying norms which are mappings from terms to the natural numbers. This paper illustrates howt o enable the use of size functions defined as tuples of these simpler norm functions. This approach enables us to simplify the problem of deriving automatically a candidate norm with which to prove termination. Instead of deriving a single, complex norm function, it is sufficient to determine a collection of simpler norms, some combination of which, leads to a proof of termination. We propose that a collection of simple norms, one for each of the recursive data-types in the program, is often a suitable choice. We first demonstrate the power of combining norm functions and then the adequacy of combining norms based on regular types.
|Titel||Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002 : Venice, Italy, January 21-22, 2002|
|Status||Udgivet - 2002|
|Navn||Lecture Notes in Computer Science|
Genaim, S., Codish, M., Gallagher, J. P., & Lagoon, V. (2002). Combining norms to prove termination. I A. Cortesi (red.), Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002 (s. 126-138). Springer. Lecture Notes in Computer Science, Bind. 2294