this paper discusses refinement of programs that may raise and catch exceptions. We show that exceptions are expressed by a class of predicate transformers built on Arieli and Avron's four-valued logic and develop...
详细信息
ISBN:
(纸本)9783642125911
this paper discusses refinement of programs that may raise and catch exceptions. We show that exceptions are expressed by a class of predicate transformers built on Arieli and Avron's four-valued logic and develop a refinement framework for the four-valued predicate transformers. the resulting framework enjoys several refinement laws that are useful for stepwise refinement of programs involving exception handling and partial predicates. We demonstrate some typical usages of the refinement laws in the proposed framework by a few examples of programtransformation.
Homeomorphic Embedding (HEm) has proven to be very powerful for supervising termination of computations, provided that such computations are performed over a finite signature, i.e., the number of constants and functio...
详细信息
ISBN:
(纸本)9783540787686
Homeomorphic Embedding (HEm) has proven to be very powerful for supervising termination of computations, provided that such computations are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are situations, for example numeric computations, which involve an infinite (or too large) signature, in which HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination, but they either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We introduce Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped HEm to deal with infinite signatures. In the paper, we show how TbHEm can be used to improve the accuracy of online partial evaluation. For this purpose, we propose an approach to constructing suitable types for partial evaluation automatically based on existing analysis tools for constraint logicprograms. We also present useful properties of types which allow us to take full advantage of TbHEm in practice. Experimental results are reported which show that our work improves the state of the practice of online partial evaluation.
Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algo...
详细信息
ISBN:
(纸本)9783540714095
Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algorithmic debugger. therefore, the performance of the technique is strongly dependent on the number and the complexity of these questions. In this work we overview and compare current strategies for algorithmic debugging and we introduce some new strategies and discuss their advantages over previous approaches.
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for t...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of programtransformationthat allows to transform logicprograms in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer su...
详细信息
ISBN:
(纸本)9783642125911
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer substitutions and termination. Moreover, modes allow us to define a somewhat declarative semantics for it and to relax some rather unpractical constraints on variable occurrences while retaining a straightforward semantics.
In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic, programming. Our method is based on a classical unfolding operation...
详细信息
ISBN:
(纸本)9783540714095
In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic, programming. Our method is based on a classical unfolding operation together with semi-unification and is independent of a particular reduction strategy. We also describe a technique to reduce the explosion of rules caused by the unfolding process. the analyser that we have implemented is able to solve most of the non-terminating examples in the Termination Problem Data Base.
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.
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augm...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.
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.
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.
暂无评论