We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerf...
详细信息
ISBN:
(纸本)9783642205507
We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to provide error symptoms in advance and is applicable with partial specifications and even partial programs.
program correctness (in imperative and functional programming) splits in logicprogramming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. L...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
program correctness (in imperative and functional programming) splits in logicprogramming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. Little work has been devoted to reasoning about completeness. this paper presents a few sufficient conditions for completeness of definite programs. We also study preserving completeness under some cases of pruning of SLD-trees (e.g. due to using the cut). We treat logicprogramming as a declarative paradigm, abstracting from any operational semantics as far as possible. We argue that the proposed methods are simple enough to be applied, possibly at an informal level, in practical Prolog programming. We point out importance of approximate specifications.
Fault-tolerance is a crucial property in many systems. thus, mechanical verification of algorithms associated withsynthesis of fault-tolerant programs is desirable to ensure their correctness. In this paper, we prese...
详细信息
ISBN:
(纸本)3540266550
Fault-tolerance is a crucial property in many systems. thus, mechanical verification of algorithms associated withsynthesis of fault-tolerant programs is desirable to ensure their correctness. In this paper, we present the mechanized verification of algorithms that automate the addition of fault-tolerance to a given fault-intolerant program using the PVS theorem prover. By this verification, not only we prove the correctness of the synthesis algorithms, but also we guarantee that any program synthesized by these algorithms is correct by construction. Towards this end, we formally define a uniform framework for formal specification and verification of fault-tolerance that consists of abstract definitions for programs, specifications, faults, and levels of fault-tolerance, so that they are independent of platform and architecture. the essence of synthesis algorithms involves fixpoint calculations. Hence, we also develop a reusable library for fixpoint calculations on finite sets in PVS.
the need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear logic (CLL) for correct-by-construction...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
the need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear logic (CLL) for correct-by-construction resource-based process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting.
there are two kinds of approaches for termination analysis of logicprograms: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logicprogram. T...
详细信息
ISBN:
(纸本)9783540714095
there are two kinds of approaches for termination analysis of logicprograms: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logicprogram. transformational approaches transform a logicprogram into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. thus, transformational approaches make all methods previously developed for TRSs available for logicprograms as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logicprograms. (Most of them are restricted to well-moded programs.) In this paper we improve these transformations such that they become applicable for any definite logicprogram. To simulate the behavior of logicprograms by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logicprograms, our technique is also sound for logicprogramming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.
Rule-based formalisms are ubiquitous in computer science. However, a difficulty that arises frequently when specifying or programming the rules is to determine which effects should be propagated by these rules. In thi...
详细信息
ISBN:
(纸本)9783540714095
Rule-based formalisms are ubiquitous in computer science. However, a difficulty that arises frequently when specifying or programming the rules is to determine which effects should be propagated by these rules. In this paper, we present a tool called ARM (Automatic Rule Miner) that generates rules for relations over finite domains. ARM offers a rich functionality to provide the user withthe possibility of specifying the admissible syntactic forms of the rules. Furthermore, we show that our approach performs well on various examples, e.g. generation of firewall rules or generation of rule-based constraint solvers. thus, it is suitable for users from different fields.
In recent work, the effectiveness of using declarative languages has been demonstrated for many problems in program analysis. Using a simple relational query language, like DATALOG, complex interprocedural analyses in...
详细信息
ISBN:
(纸本)9783642125911
In recent work, the effectiveness of using declarative languages has been demonstrated for many problems in program analysis. Using a simple relational query language, like DATALOG, complex interprocedural analyses involving dynamically created objects can be expressed in just a few lines. By exploiting the power of the Rewriting logic language MAUDE, we aim at transforming DATALOG programs into efficient rewrite systems that compute the same answers. A prototype has been implemented and applied to some real-world DATALOG-based analyses. Experimental results show that the performance of solving DATALOG queries in rewriting logic is comparable to state-of-the-art DATA LOG solvers.
In this paper we propose a novel semi-supervised active machine-learning method, based on two recursive higher-order functions that can inductively synthesize a functional computer program. based on properties formula...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
In this paper we propose a novel semi-supervised active machine-learning method, based on two recursive higher-order functions that can inductively synthesize a functional computer program. based on properties formulated using abstract algebra terms, the method uses two combined strategies: to reduce the dimensionality of the Boolean algebra where a target function lies and to combine known operations belonging to the algebra, using them as a basis to build a programthat emulates the target function. the method queries for data on specific points of the problem input space and build a programthat exactly fits the data. Applications of this method include all sorts of systems based on bitwise operations. Any functional computer program can be emulated using this approach. Combinatorial circuit design, model acquisition from sensor data, reverse engineering of existing computer programs are all fields where the proposed method can be useful.
We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logicprograms. the new condition of negative unfolding is a natural one, since ...
详细信息
ISBN:
(纸本)9783642125911
We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logicprograms. the new condition of negative unfolding is a natural one, since it is considered as a special case of replacement rule. the correctness of our unfold/fold transformation system in the sense of the perfect model semantics is proved. We then consider the coinductive proof rules proposed by Jaffar et al. We show that our unfold/fold transformation system, when used together with Lloyd-Topor transformation, can prove a proof problem which is provable by the coinductive proof rules by Jaffar et al. To this end, we propose a new replacement rule, called sowed replacement, which is not necessarily equivalence-preserving, but is essential to perform a reasoning step corresponding to coinduction.
Conjunctive partial deduction is a well-known technique for the partial evaluation of logicprograms. the original formulation follows the so called online approach where all termination decisions are taken on-the-fly...
详细信息
ISBN:
(纸本)9783642205507
Conjunctive partial deduction is a well-known technique for the partial evaluation of logicprograms. the original formulation follows the so called online approach where all termination decisions are taken on-the-fly. In contrast, offline partial evaluators first analyze the source program and produce an annotated version so that the partial evaluation phase should only follow these annotations to ensure the termination of the process. In this work, we introduce a lightweight approach to conjunctive partial deduction that combines some of the advantages of both online and offline styles of partial evaluation.
暂无评论