Letonchanh's List: Termination

• There is an implicit 0-th element to each function measure, called the “level” of the function.
• Call cycles (i.e., groups of functions which are allowed to call each other recursively, subject to non-level measure decrease) need to be declared explicitly.
• strongly connected components
• If VCC sees the entire call graph, it will infer correct levels.

2 more annotations...