A Counterexample-Guided Debugger for Non-recursive Datalog
A Counterexample-Guided Debugger for Non-recursive Datalog
复制标题
用于非递归数据记录的反例引导调试器
DOI：
10.1007/978-3-030-64437-6_17
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Hu Zhenjiang
中科院分区：
文献类型：
--
作者：
Tran Van-Dang;Kato Hiroyuki;Hu Zhenjiang
Datasheet语言用于许多潜在的应用，包括数据库查询、程序分析、双向转换等。在实践中，这样一个数据库程序被期望写得很好，以满足要求，如双向编程中的往返属性。虽然验证和调试Datasheet程序起着至关重要的作用，以保证这些程序的预期性能，很少的方法已经提出。现有的方法需要用户花费大量的精力来发现数据库程序的非预期行为或意外计算，既没有提供反例也没有提供错误解释。在本文中，我们提出了一个有效的方法，以交互式调试的数据库程序，使用户的负担减轻。具体来说，我们提供了一个语法为用户指定的属性的非递归Datasheet程序，提出了一个反例生成器，验证指定的属性，并产生反例，以显示意外的行为，用户编写的程序，并设计了一个调试引擎结合基于对话框的用户界面，以帮助用户在定位程序中的错误与生成的反例。我们已经实现了我们的方法的原型，并证明了其可行性和效率。
The Datalog language is used in many potential applications including database queries, program analysis, bidirectional transformations, and so forth. In practice, such a Datalog program is expected to be well-written to meet requirements such as the round-tripping properties in bidirectional programming. Although verifying and debugging Datalog programs play an essential role to guarantee the expected properties of these programs, very few approaches have been proposed. The existing approaches require much users’ effort in finding out unintended behaviors or unexpected computations of the Datalog program that neither counterexamples nor bug explanations are provided. In this paper, we propose an efficient approach to interactively debugging Datalog programs so that the user’s burden is reduced. Specifically, we provide a syntax for users to specify properties of non-recursive Datalog programs, present a counterexample generator that verifies specified properties and generates counterexamples to show unexpected behaviors of user-written programs, and design a debugging engine combined with a dialog-based user interface to assist users in locating bugs in the programs with the generated counterexamples. We have implemented a prototype of our approach and demonstrated its feasibility and efficiency.