Examinando Termination por Título
Mostrando 1 - 2 de 2
Resultados por página
Opciones de ordenación
ResumenTermination Analysis in a Multi-language Verification PlatformHolubanský, Jakub; Mínguez, Álvaro; Peña Marí, Ricardo. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.One aim of the verification platform CAVI-ART is to provide as much assistance as possible to programmers in order to alleviate their verification effort. One of these aids is automatically proving termination of programs, whenever this is possible. Since CAVI-ART is a multi-language platform, the analysis is performed at the level of the platform Intermediate Representation language (IR), to which all source languages are first translated. We have selected one of the the most successful termination tools, called RANK, and transform our IR-programs to an appropriate input for RANK. There is a fundamental mismatch between the functional, stateless, recursive flavour of our IR, and the automaton-based input of RANK, which is a tool developed for imperative, mutable-state programs. In this paper we show how we have circumvented this problem, and present an algorithm transforming the IR to an automaton. We give some examples of recursive programs that we have successfully proved terminating. ResumenUse of logical models for proving operational termination in general logicsLucas, Salvador. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.A declarative programming language is based on some logic L and its operational semantics is given by a proof calculus which is often presented in a natural deduction style by means of inference rules. Declarative programs are theories S of L and executing a program is proving goals G in the inference system I(S) associated to S as a particularization of the inference system of the logic. The usual soundness assumption for L implies that every model M of S also satisfies G. In this setting, the operational termination of a declarative program is quite naturally defined as the absence of infinite proof trees in the inference system I(S). Proving operational termination of declarative programs often involves two main ingredients: (i) the generation of logical models M to abstract the program execution (i.e., the provability of specific goals in I(S)), and (ii) the use of well-founded relations to guarantee the absence of infinite branches in proof trees and hence of infinite proof trees, possibly taking into account the information about provability encoded by M. In this paper we show how to deal with (i) and (ii) in a uniform way. The main point is the synthesis of logical models where well-foundedness is a side requirement for some specific predicate symbols.