Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation originally developed for logicprogramming can be extended and applied to prove the validity of fixpoint logic formulas. In the present paper, we refine their unfold/fold transformation, so that each predicate can be unfolded a different number of times in an asynchronous manner. Inspired by the work of Lee et al. on size change termination, we use a variant of size change graphs to find an appropriate number of unfoldings of each predicate. We have implemented an unfold/fold transformation tool based on the proposed method, and evaluated its effectiveness.
Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a programthe type of which ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a programthe type of which is a given formula. We present a model of automata that can handle proof construction in full intuitionistic first-order logic. the automata are constructed in such a way that any successful run corresponds directly to a normal proof in the logic. this makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections withthe traditional logical connectives.
Higher-order logicprogramming is an interesting extension of traditional logicprogramming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order charact...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
Higher-order logicprogramming is an interesting extension of traditional logicprogramming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higher-order logicprograms and can transform them into first-order programs without introducing additional data structures. the resulting first-order programs can be executed by conventional logicprogramming interpreters and benefit from other optimizations that might be available. We provide an implementation and experimental results that suggest the efficiency of the transformation.
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this pape...
详细信息
ISBN:
(纸本)9783540787686
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this paper, we describe an implementation based on source-to-source transformations to CHR (extended with some low-level compiler directives). We allow user-defined aggregates and nested aggregate expressions over arbitrary guarded conjunctions of constraints. Both an on-demand and an incremental aggregate computation strategy are supported.
Proving termination of, or generating efficient control for Constraint Handling Rules (CH R,) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to L...
详细信息
ISBN:
(纸本)9783642125911
Proving termination of, or generating efficient control for Constraint Handling Rules (CH R,) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to logicprogramming (LP), there are not many tools available for deriving such information for CHR. Hence, instead of building analyses for CHR from scratch, we define a, transformation from CHR to Prolog and reuse existing analysis tools for Prolog. the proposed transformation has been implemented and combined with Poly Types 1.3, a type analyser for Prolog, resulting in an accurate description of the types of CHR programs. Moreover, the transformation is not limited to type analysis. It can also be used to prove other properties of the constraints showing up in constraint stores, using tools for Prolog.
Termination of binary CLP programs has recently become an important question in the termination analysis community. the reason for this is due to the fact that some of the recent approaches to termination of logic pro...
详细信息
ISBN:
(纸本)3540266550
Termination of binary CLP programs has recently become an important question in the termination analysis community. the reason for this is due to the fact that some of the recent approaches to termination of logicprograms abstract the input program to a binary CLP program and conclude termination of the input program from termination of the abstracted program. In this paper we introduce a class of binary CLP programs such that their termination can be proved by using linear level mappings. We show that membership to this class is decidable and present a decision procedure. Further, we extend this class to programs such that their termination proofs require a combination of linear functions. In particular we consider as level mappings tuples of linear functions and piecewise linear functions.
Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-ge...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to assoc...
详细信息
ISBN:
(纸本)3540266550
In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to associate a symbolic cost to each basic operation (e.g., variable updates, function unfoldings, case evaluations). While this cost semantics provides a formal basis to analyze the cost of a computation, the implementation of a cost-augmented interpreter based on it would introduce a huge overhead. therefore, we also introduce a sound transformationthat instruments a program such that its execution-under the standard semantics-yields not only the corresponding results but also the associated costs. Finally, we describe a prototype implementation of a profiler based on the developments in this paper.
logicprogramming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, w...
详细信息
ISBN:
(纸本)9783031712937;9783031712944
logicprogramming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, we present a method to use functions to improve the operational behavior of logicprograms without loosing the flexibility of logicprogramming. For this purpose, predicates and goals are transformed into functions and nested expressions. By evaluating these functions in a demand-driven manner wherever possible and taking potential failures into account, we ensure that the execution of the transformed programs will never require more steps than the original programs but can decrease the number of steps-in the best case reducing infinite search spaces to finite ones. thus, we obtain a systematic method to improve the operational behavior of logicprograms without changing their semantics.
In recent years techniques and systems have been developed to prove non-termination of logicprograms for certain classes of queries. In previous work, we developed such a system based on mode-information and a form o...
详细信息
ISBN:
(纸本)9783642205507
In recent years techniques and systems have been developed to prove non-termination of logicprograms for certain classes of queries. In previous work, we developed such a system based on mode-information and a form of loop checking performed at compile time. In the current paper we improve this technique by integrating type information in the analysis and by applying non-failure analysis and program specialization. It turns out that there are several classes of programs for which existing non-termination analyzers fail and for which our extended technique succeeds in proving non-termination.
暂无评论