检索结果-内蒙古大学图书馆

declarative debugging Meets the World

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2008年第C期216卷 65-77页

作者： Lux, Wolfgang Univ Munster Munster Germany

declarative debugging has been proposed as a suitable technique for diagnosing errors. It is particularly attractive for declarative programming languages, whose operational semantics differs substantially from their declarative semantics. declarative debuggers are usually described and implemented by means of a program transformation. However, this transformation does not mix well with monadic I/O, which is used by lazy functional and functional logic languages. Therefore, declarative debuggers for such languages either do not support debugging of programs involving stateful computations at all, or require special support from the compiler and its runtime system. In this paper, we present a modified program transformation that blends nicely with monadic I/O and therefore covers the whole language without additional support from the target implementation.

关键词： declarative debugging monadic I/O

来源：评论

学校读者我要写书评

暂无评论

declarative debugging of rewriting logic specifications

引用

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING 2012年第7-8期81卷 851-897页

作者： Riesco, Adrian Verdejo, Alberto Marti-Oliet, Narciso Caballero, Rafael Univ Complutense Madrid Fac Informat Dpto Sistemas Informat & Computac E-28040 Madrid Spain

declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows one to state membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, which correspond to transitions between states and can be nondeterministic. We propose here a calculus to infer reductions, sort inferences, normal forms, and least sorts with the equational subset of rewriting logic, and rewrites and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for both wrong (an incorrect result obtained from an initial result) and missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented Maude DDebugger, a declarative debugger for Maude. a high-performance system based on rewriting logic. We illustrate its use with an example. (C) 2011 Elsevier Inc. All rights reserved.

关键词： declarative debugging Rewriting logic Maude Wrong answers Missing answers

来源：评论

学校读者我要写书评

暂无评论

declarative debugging OF MISSING ANSWERS FOR MAUDE SPECIFICATIONS

DECLARATIVE DEBUGGING OF MISSING ANSWERS FOR MAUDE SPECIFICA...

引用

21st International Conference on Rewriting Techniques and Applications (RTA) as part of the 5th International Federated Logic Conference (FLOC)

作者： Riesco, Adrian Verdejo, Alberto Marti-Oliet, Narciso Univ Complutense Madrid Fac Informat Madrid Spain

ISBN: (纸本)9783939897187

declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows to state of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.

关键词： declarative debugging Maude Missing answers Rewriting Logic

来源：评论

学校读者我要写书评

暂无评论

Using Big-Step and Small-Step Semantics in Maude to Perform declarative debugging

Using Big-Step and Small-Step Semantics in Maude to Perform ...

引用

12th International Symposium on Functional and Logic Programming (FLOPS)

作者： Riesco, Adrian Univ Complutense Madrid Dept Sistemas Informat & Comp Madrid Spain

ISBN: (纸本)9783319071510;9783319071503

declarative debugging is a semi-automatic debugging technique that abstracts the execution details to focus on results. This technique builds a debugging tree representing an incorrect computation and traverses it by asking questions to the user until the error is found. In previous works we have presented a declarative debugger for Maude specifications. Besides a programming language, Maude is a semantic framework where several other languages can be specified. However, our declarative debugger is only able to find errors in Maude specifications, so it cannot find bugs on the programs written on the languages being specified. We study in this paper how to modify our declarative debugger to find this kind of errors when defining programming languages using big-step and small-step semantics, two generic approaches that allow to specify a wide range of languages in a natural way. We obtain our debugging trees by modifying the proof trees obtained from the semantic rules. We have extended our declarative debugger to deal with this kind of debugging, and we illustrate it with an example.

关键词： declarative debugging Big-step semantics Small-step semantics Maude

来源：评论

学校读者我要写书评

暂无评论

A unified framework for declarative debugging and testing

引用

INFORMATION AND SOFTWARE TECHNOLOGY 2021年 129卷 106427-106427页

作者： Caballero, Rafael Martin-Martin, Enrique Riesco, Adrian Tamarit, Salvador Univ Complutense Madrid Dept Sistemas Informat & Computac Fac Informat C Prof Jose Garcia Santesmases 9 Madrid 28040 Spain Univ Politecn Valencia Dept Sistemes Informat & Comp Cami Vera S-N Valencia 46022 Spain

Context: debugging is the most challenging and time consuming task in software development. However, it is not properly integrated in the software development cycle, because the result of so much effort is not available in further iterations of the cycle, and the debugging process itself does not benefit from the outcome of other phases such as testing. Objective: We propose to integrate debugging and testing within a single unified framework where each phase generates useful information for the other and the outcomes of each phase are reused. Method: We consider a declarative debugging setting that employs tests to automatically entail the validity of some subcomputations, thus decreasing the time and effort needed to find a bug. Additionally, the debugger stores as new tests the information collected from the user during the debugging phase. This information becomes part of the program test suite, and can be used in future debugging sessions, and also as regression tests. Results: We define a general framework where declarative debugging establishes a bidirectional collaboration with testing. The new setting preserves the properties of the underlying declarative debugging framework (weak completeness and soundness) while generating test cases that can be used later in other debugging sessions or even in other cycles of the software development. The proposed framework is general enough to be instantiated to very different programming languages: Erlang (functional), Java (imperative, object-oriented), and SQL (data query);and the experimental results obtained for Erlang programs validate the effectiveness of the framework. Conclusion: We propose a general unified framework for debugging and testing that simplifies each phase and maximizes the reusability of the outcomes in the different phases of the software development cycle, therefore reducing the overall effort.

关键词： Property-based testing Unit testing declarative debugging Unified framework

来源：评论

学校读者我要写书评

暂无评论

A three-valued semantics for logic programmers

引用

THEORY AND PRACTICE OF LOGIC PROGRAMMING 2006年第0期6卷 509-538页

作者： Naish, Lee Univ Melbourne Dept Comp Sci & Software Engn Melbourne Vic 3010 Australia

This paper describes a simpler way for programmers to reason about the correctness of their code. The study of semantics of logic programs has shown strong links between the model theoretic semantics (truth and falsity of atoms in the programmer's interpretation of a program), procedural semantics (for example, SLD resolution) and fixpoint semantics (which is useful for program analysis and alternative execution mechanisms). Most of this work assumes that intended interpretations are two-valued: a ground atom is true (and should succeed according to the procedural semantics) or false (and should not succeed). In reality, intended interpretations are less precise. Programmers consider that some atoms "should not occur" or are "ill-typed" or "inadmissible". Programmers don't know and don't care whether such atoms succeed. In this paper we propose a three-valued semantics for (essentially) pure Prolog programs with (ground) negation as failure which reflects this. The semantics of Fitting is similar but only associates the third truth value with non-termination. We provide tools to reason about correctness of programs without the need for unnatural precision or undue restrictions on programming style. As well as theoretical results, we provide a programmer-oriented synopsis. This work has come out of work on declarative debugging, where it has been recognised that inadmissible calls are important.

关键词： models immediate consequence operator SLDNF resolution negation verification declarative debugging inadmissibility

来源：评论

学校读者我要写书评

暂无评论

Transforming floundering into success

引用

THEORY AND PRACTICE OF LOGIC PROGRAMMING 2014年第2期14卷 215-238页

作者： Naish, Lee Univ Melbourne Melbourne Sch Engn Dept Comp & Informat Syst Melbourne Vic 3010 Australia

We show how logic programs with "delays" can be transformed to programs without delays in a way that preserves information concerning floundering (also known as deadlock). This allows a declarative (model-theoretic), bottom-up or goal-independent approach to be used for analysis and debugging of properties related to floundering. We rely on some previously introduced restrictions on delay primitives and a key observation which allows properties such as groundness to be analysed by approximating the (ground) success set.

关键词： floundering delays coroutining program analysis abstract interpretation program transformation declarative debugging

来源：评论

学校读者我要写书评

暂无评论

A declarative framework for stateful analysis of execution traces

引用

SOFTWARE QUALITY JOURNAL 2017年第1期25卷 201-229页

作者： Wininger, Florian Ezzati-Jivan, Naser Dagenais, Michel R. Ecole Polytech Montreal Montreal PQ H3T 1J4 Canada

With newer complex multi-core systems, it is important to understand an application's runtime behavior to be able to debug its execution, detect possible problems and bottlenecks and finally identify potential root causes. Execution traces usually contain precise data about an application execution. Their analysis and abstraction at multiple levels can provide valuable information and insights about an application's runtime behavior. However, with multiple abstraction levels, it becomes increasingly difficult to find the exact location of detected performance or security problems. Tracing tools provide various analysis views to help users to understand their application problems. However, these pre-defined views are often not sufficient to reveal all analysis aspects of the underlying application. A declarative approach that enables users to specify and build their own custom analysis and views based on their knowledge, requirements and problems can be more useful and effective. In this paper, we propose a generic declarative trace analysis framework to analyze, comprehend and visualize execution traces. This enhanced framework builds custom analyses based on a specified modeled state, extracted from a system execution trace and stored in a special purpose database. The proposed solution enables users to first define their different analysis models based on their application and requirements, then visualize these models in many alternate representations (Gantt chart, XY chart, etc.), and finally filter the data to get some highlights or detect some potential patterns. Several sample applications with different operating systems are shown, using trace events gathered from Linux and Windows, at the kernel and user-space levels.

关键词： Software debugging declarative debugging Execution trace analysis

来源：评论

学校读者我要写书评

暂无评论

A zoom-declarative debugger for sequential Erlang programs

引用

SCIENCE OF COMPUTER PROGRAMMING 2015年 110卷 104-118页

作者： Caballero, Rafael Martin-Martin, Enrique Riesco, Adrian Tamarit, Salvador Univ Complutense Madrid Fac Informat Dept Sistemas Informat & Computac E-28040 Madrid Spain Univ Politecn Madrid Fac Informat Babel Res Grp Boadilla Del Monte 28660 Spain

We present a declarative debugger for sequential Erlang programs. The tool is started when a program produces some unexpected result, and proceeds asking questions to the user about the correctness of some subcomputations until an erroneous program function is found. Then, the user can refine the granularity by zooming in the function, checking the values bound to variables and the if/case/try-catch branches taken during the execution. We show by means of an extensive benchmark that the result is a usable, scalable tool that complements already existing debugging tools such as the Erlang tracer and Dialyzer. Since the technique is based on a formal calculus, we are able to prove the soundness and completeness of the approach. (C) 2015 Elsevier B.V. All rights reserved.

关键词： Erlang Zoom debugging declarative debugging

来源：评论

学校读者我要写书评

暂无评论

Truth versus information in logic programming

引用

THEORY AND PRACTICE OF LOGIC PROGRAMMING 2014年第6期14卷 803-840页

作者： Naish, Lee Sondergaard, Harald Univ Melbourne Dept Comp & Informat Syst Melbourne Vic 3010 Australia

The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood but also for "undefined". The three-valued semantics proposed by Fitting (Fitting, M. 1985. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming 2, 4, 295-312) and Kunen (Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4, 4, 289-308) are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being associated with underspecification. Naish used an (apparently) novel "arrow" operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Belnap's four-valued logic (Belnap, N. D. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, J. M. Dunn and G. Epstein, Eds. D. Reidel, Dordrecht, Netherlands, 8-37), also used elsewhere by Fitting, to unify the two three-valued approaches. The truth values are arranged in a bilattice, which supports the classical ordering on truth values as well as the "information ordering". We note that the "arrow" operator of Naish (and our four-valued extension) is essentially the information ordering, whereas the classical arrow denotes the truth ordering. This allows us to shed new light on many aspects of logic programming, including program analysis, type and mode systems, declarative debugging and the relationships between specifications and programs, and successive execution states of a program.

关键词： declarative debugging information order intended interpretation logic program specification many-valued logic modes program analysis specification semantics

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：