Motivation

Termination can be thought of as the property of programs ensuring that every input is given an output in finite time. There are many programming languages, with different features and expressive resources and programs of different shapes. Is a common formal definition of termination of programs in any (or most) of these programming languages possible? Are there common approaches, methods, and tools for automatically proving termination?

The notion of operational termination provides a general definition of termination which relies on the logic-based description of the operational semantics of a programming language. The key point is capturing termination as the absence of infinite inference: all proof attempts must either successfully terminate, or else fail in finite time.

This global notion is well-suited for most declarative languages, where programs are theories in a logic. Other programming languages (e.g., imperative languages) and applications (e.g., the evaluation of specific expressions and goals in functional and logic programs) require a more specialized treatment which pays attention to specific formulas to be proved within a given theory.

We can, however, treat them all essentially in the same way, with a common methodology which is well-suited for implementation and automation of termination proofs.

The tutorial

The tutorial develops a generic and unifying approach to prove termination of programs in a wide range of programming languages. The starting point is a description of the operational semantics of the programming language given by means of a computational logic. The notion of (localized) operational termination [1,3] provides an appropriate semantics-based definition of termination of programs as the absence of infinite proof trees in the logic. By using a number of generic methods and procedures (see [2,3]) we obtain a unified description of the termination problem as what we call an OT problem. Then, we apply an incremental proof methodology which is able to simplify the original OT problem in a divide-and-conquer style to eventually prove (or disprove) termination of the program. We also discuss some low-level aspects of the methodology as the use of fine-grain models of the termination behavior in some languages, and the use of abstractions, search, and automated reasoning techniques in the implementation of the aforementioned proof methodology [4].

Get the slides of the tutorial!

References

[1] Salvador Lucas, Claude Marché and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446-453, 2005.

[2] Salvador Lucas and José Meseguer. Proving Termination of Declarative Programs in General Logics. In Proc. of the 16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014, pages 111-122, ACM 2014.

[3] Salvador Lucas and José Meseguer. Localized Operational Termination in General Logics. In Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Lecture Notes in Computer Science, volume 8950, pages 91-114, to appear, 2015.

[4] Salvador Lucas and José Meseguer. Models for Logics and Conditional Constraints in Automated Proofs of Termination. In Proc. of the 12th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2014. Lecture Notes in Computer Science, volume 8884, pages 9-20, Springer-Verlag, 2014.