While past research in answer-set programming (ASP) mainly focused on theory, ASP solver technology, and applications, the present work situates itself in the context of a quite recent research trend: development support for ASP. In particular, we propose to augment answer-set programs with additional meta-information formulated in a dedicated annotation language, called LANA. This language allows the grouping of rules into coherent blocks and to specify language signatures, types, pre- and postconditions, as well as unit tests for such blocks. While these annotations are invisible to an ASP solver, as they take the form of program comments, they can be interpreted by tools for documentation, testing, and verification purposes, as well as to eliminate sources of common programming errors by realising syntax checking or code completion features. To demonstrate its versatility, we introduce two such tools, viz. (i) ASPDOC, for generating an HTML documentation for a program based on the annotated information, and (ii) ASPUNIT, for running and monitoring unit tests on program blocks. LANA is also exploited in the SeaLion system, an integrated development environment for ASP based on Eclipse. To appear in Theory and Practice of Logic Programming
In general, developing and debugging a declarative language is quite different from software engineering in a more traditional procedural or object-oriented programming language. With larger programs for real-world applications being written, it is vital to support the programmer with the right tools. In recent years, some work has been done to provide the ASP programmer with dedicated tools. The integrated development environments @cite_22 and @cite_21 provide, among other features, syntax colouring and syntax checking for ASP programs and run as an Eclipse front-end to solvers. IDEs for the solver and its extensions are discussed by peritecive07 and aspide . Debugging in ASP is supported by @cite_20 , which makes use of ASP to explain and handle unexpected outcomes like missing atoms in an answer set or the absence of an answer set. aspviz and kara provide mechanisms to visualise answer sets of a given program to support code debugging.
@cite_21 @cite_22 @cite_20
2171836055 2624790684 1597298151 2169808787
Answer-set programming (ASP) is widely recognised as a viable tool for declarative problem solving. However, there is currently a lack of tools for developing answer-set programs. In particular, providing tools for debugging answer-set programs has recently been identified as a crucial prerequisite for a wider acceptance of ASP. In this paper, we introduce a meta-programming technique for debugging in ASP. The basic question we address is why interpretations expected to be answer sets are not answer sets of the program to debug. We thus deal with finding semantical errors of programs. The explanations provided by our method are based on an intuitive scheme of errors that relies on a recent characterisation of the answer-set semantics. Furthermore, as we are using a meta-programming technique, debugging queries are expressed in terms of answer-set programs themselves, which has several benefits: For one, we can directly use ASP solvers for processing debugging queries. Indeed, our technique can easily be implemented, and we devised a corresponding prototype debugging system. Also, our approach respects the declarative nature of ASP, and the capabilities of the system can easily be extended to incorporate differing debugging features. Answer-set programming (ASP) is a logic programming paradigm for declarative problem solving which gained increasing importance during the last decade. However, so far hardly any tools exist supporting software engineers in developing answer-set programs, and there are no standard methodologies for handling unexpected outcomes of a program. Thus, writing answer-set programs is sometimes quite intricate, especially when large programs for real-world applications are required. In order to increase the usability of ASP, the development of appropriate debugging strategies is therefore vital. In this paper, we describe the system spock, a debugging support tool for answer-set programs making use of ASP itself. The implemented techniques maintain the declarative nature of ASP within the debugging process and are independent from the actual computation of answer sets. Answer Set Programming is a well-established paradigm of declarative programming in close relationship with other declarative formalisms such as SAT Modulo Theories, Constraint Handling Rules, FO(.), PDDL and many others. Since its first informal editions, ASP systems are compared in the nowadays customary ASP Competition. The Third ASP Competition, as the sequel to the ASP Competitions Series held at the University of Potsdam in Germany (2006-2007) and at the University of Leuven in Belgium in 2009, took place at the University of Calabria (Italy) in the first half of 2011. Participants competed on a selected collection of declarative specifications of benchmark problems, taken from a variety of domains as well as real world applications, and instances thereof. The Competition ran on two tracks: the Model & Solve Competition, held on an open problem encoding, on an open language basis, and open to any kind of system based on a declarative specification paradigm; and the System Competition, held on the basis of fixed, public problem encodings, written in a standard ASP language. This paper briefly discuss the format and rationale of the System competition track, and preliminarily reports its results. Answer set programming (ASP) with disjunction offers a powerful tool for declaratively representing and solving hard problems. Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise and intuitive way, where the encoding reflects the typical “guess and check” nature of NP problems: The property is encoded in a way such that polynomial size certificates for it correspond to stable models of a program. However, the problem-solving capacity of full disjunctive logic programs (DLPs) is beyond NP, and captures a class of problems at the second level of the polynomial hierarchy. While these problems also have a clear “guess and check” structure, finding an encoding in a DLP reflecting this structure may sometimes be a non-obvious task, in particular if the “check” itself is a co-NP-complete problem; usually, such problems are solved by interleaving separate guess and check programs, where the check is expressed by inconsistency of the check program. In this paper, we present general transformations of head-cycle free (extended) disjunctive logic programs into stratified and positive (extended) disjunctive logic programs based on meta-interpretation techniques. The answer sets of the original and the transformed program are in simple correspondence, and, moreover, inconsistency of the original program is indicated by a designated answer set of the transformed program. Our transformations facilitate the integration of separate “guess” and “check” programs, which are often easy to obtain, automatically into a single disjunctive logic program. Our results complement recent results on meta-interpretation in ASP, and extend methods and techniques for a declarative “guess and check” problem solving paradigm through ASP.