399 research outputs found
On proving left termination of constraint logic programs
No full textThe Constraint Logic Programming (CLP) Scheme merges logic programming with constraint solving over predefined domains. In this article, we study proof methods for universal left termination of constraint logic programs. We provide a sound and complete characterization of left termination for ideal CLP languages which generalizes acceptability of logic programs. The characterization is then refined to the notion of partial acceptability, which is well suited for automatic modular inference. We describe a theoretical framework for automation of the approach, which is implemented. For nonideal CLP languages and without any assumption on their incomplete constraint solvers, even the most basic sound termination criterion from logic programming does not lift. We focus on a specific system, namely CLP(R), by proposing some additional conditions that make (partial) acceptability sound
cTI: a Constraint-Based Termination Inference Tool for ISO-Prolog
No full textWe present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity
Débat. Y. Benot, M. Dorigny, B. Gainot, F. Gauthier, J.-C. Halpern, E. Mesnard, P.F. Tavares
No full textDébat. Y. Benot, M. Dorigny, B. Gainot, F. Gauthier, J.-C. Halpern, E. Mesnard, P.F. Tavares. In: Annales historiques de la Révolution française, n°297, 1994. pp. 591-593
MMlles F. Leclercq, С Marandet, MM. R. Alix, L. Cognet, J. Mesnard, R. Sève, Clermont, ville de Pascal
No full textDeyon Pierre. MMlles F. Leclercq, С Marandet, MM. R. Alix, L. Cognet, J. Mesnard, R. Sève, Clermont, ville de Pascal. In: Annales. Economies, sociétés, civilisations. 18ᵉ année, N. 2, 1963. pp. 387-390
Typing linear constraints for moding CLP(R) programs
No full textWe present a type system for linear constraints over reals and its use in mode analysis of CLP programs. The type system is designed to reason about the properties of definiteness, lower and upper bounds of variables of a linear constraint. Two proof procedures are presented for checking validity of type assertions. The first one considers lower and upper bound types, and it relies on solving homogeneous linear programming problems. The second procedure, which deals with definiteness as well, relies on computing the Minkowski’s form of a parameterized polyhedron. The two procedures are sound and complete. We extend the approach to deal with strict inequalities and disequalities. Type assertions are at the basis of moding constraint logic programs. We extend the notion of well-moding from pure logic programming to CLP(R)
A Termination Analyzer for Java Bytecode based on Path-Length
No full textIt is important to prove that supposedly terminating programs actuallyterminate, particularly if those programs must berun on critical systems or downloaded into a client such as a mobile phone.Although termination of computer programs is generally undecidable,it is possible and useful to provetermination of a large, non-trivial subset of the terminating programs.In this paper we present our termination analyser for sequential Java bytecode,based on a program property called path-length. We describe theanalyses which are needed before the path-length can be computed, such assharing, cyclicity and aliasing. Then weformally define the path-length analysis and prove it correct wrt areference denotational semantics of the bytecode. We show that a constraintlogic program P_CLPcan be built from the result of the path-length analysisof a Java bytecode program P andformally prove that if P_CLP terminates then also P terminates.Hence a termination prover for constraint logic programs can be appliedto prove the termination of P. We conclude with some discussion of thepossibilities and limitations of our approach.Ours is the first existing termination analyser for Java bytecodedealing with any kind of data structures dynamically allocated on the heapand which does not require any help or annotation on the part of the user
A new look at the automatic synthesis of linear ranking functions
No full textAbstractThe classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers
Using CLP Simplifications to Improve Java Bytecode Termination Analysis
No full textIn an earlier work, a termination analyzer for Java bytecode was developed that translates a Java bytecode program into a constraint logic program and then proves the termination of the latter. An efficiency bottleneck of the termination analyzer is the construction of a proof of termination for the generated constraint logic program, which is often very large in size. In this paper, a set of programsimplifications are presented that reduce the size of the constraint logic program without changing its termination behavior. These simplifications remove program clauses and/or predicate arguments that do not affect the termination behavior of the constraint logic program. Their effect is to reduce significantly the time needed to build the termination proof for the constraint logic program, as our experiments show
Détection des fonctions de rang linéaires à terme
No full textLa terminaison des programmes est un sujet actif de recherche en informatique. Ces dernières années ont vu l’apparition d’analyseurs de terminaison performants pour des langages comme C ou Java où l’emploi des techniques et outils de la programmation par contraintes est omniprésent. Dans cet article, nous rappelons un algorithme particulier basé sur l’emploi du lemme de Farkas pour le calcul de fonctions de rang linéaires garantissant la terminaison d’une certaine classe de boucles. Puis nous présentons une extension de cette méthode pour la découverte de fonctions linéaires qui deviennent des fonctions de rang linéaire à terme, c.-à-d. après un certain nombre de passages dans la boucle. Nous montrons la correction et la complétude d’un algorithme polynomial pour ce problème
- …
