Stepwise debugging in answer-set programming : theoretical foundations and practical realisation

Abstract

Die Antwortmengenprogrammierung (engl. answer-set programming - ASP) ist ein Programmierparadigma für deklaratives Problemlösen. Existierende Ansätze für das Debuggen von Antwortmengenprogrammen, also das Problem des Auffindens von Fehlern in Antwortmengenprogrammen, weisen Einschränkungen bezüglich ihrer praktischen Anwendbarkeit auf. Insbesondere werden wichtige Teile des Sprachumfangs von modernen ASP Solvern nicht abgedeckt und oftmals ist die Menge an Informationen sehr hoch, die dem System bereitgestellt werden muss oder mit der die Benutzerin oder der Benutzer konfrontiert wird. In dieser Dissertation wird die Stepping Methodologie für ASP eingeführt, eine neue Technik für das Debuggen von Antwortmengenprogrammen die allgemein genug ist um auf verschiedene ASP Solver Sprachen angewandt zu werden. Unsere Methode erlaubt es dem Benutzer oder der Benutzerin der eigenen Intuition zu folgen um zu entscheiden welche Regel als nächstes betrachtet werden soll. Auf diese Weise ist es möglich sich von Anfang an auf interessante Bereiche des Debugging Suchraums zu fokussieren. Programmierfehler können gefunden werden, indem eine Stepping Sitzung Unterschiede zwischen der tatsächlichen Semantik eines Programms und der Intuition des Benutzers oder der Benutzerin aufzeigt. Um die Stepping Technik auf eine solide theoretische Grundlage zu stellen, haben wir ein formales Rahmenwerk für Berechnungen von Antwortmengenprogrammen entwickelt. Damit dieses aktuelle ASP Solver Sprachen tatsächlich vollständig unterstützt, mussten wir mehrere Herausforderungen bewältigen. Eine wesentliche Schwierigkeit hierbei ist, dass sich die Sprachen von ASP Solvern sowohl voneinander als auch von formalen ASP Sprachen unterscheiden. Um eine Methode zu entwickeln die für mehrere Solver funktioniert, benötigten wir daher eine abstrakte ASP Sprache die allgemein genug ist um verschiedene Solver Sprachen abzudecken. Zu diesem Zweck greifen wir auf Abstract Constraints zurück, einer etablierten Abstraktion von beliebten Sprachkonstrukten wie beispielsweise Aggregaten. Keine existierende Semantik für die Zielsprache war mit den Semantiken aller Solver die wir unterstützen wollen kompatibel. Aus diesem Grund führen wir in dieser Arbeit eine solche Semantik ein und zeigen einige ihrer Eigenschaften. Darüber hinaus stellen wir verschiedene Charakterisierungen der neuen Semantik vor die für unser Berechnungsmodell wichtig sind. Die Stepping Technik wurde in SeaLion implementiert, einer integrierten Entwicklungsumgebung für ASP die im selben Kontext wie diese Dissertation entstand, nämlich im Rahmen eines Forschungsprojektes über Methoden und Methodologien zur Enwicklung von Antwortmengenprogrammen. Wir stellen die Hauptkomponenten von SeaLion vor und beschreiben unseren Ansatz anhand verschiedener Beispiel Szenarien wie Stepping für Antwortmengenprogramme in den Sprachen von Gringo und DLV darin verwendet werden kann. Außerdem diskutieren wir methodologische Aspekte und die Einbettung von Stepping im ASP Entwicklungsprozess.

This thesis deals with debugging in answer-set programming (ASP). Previous approaches for finding errors in answer-set programs come with limited practical applicability as they do not cover important aspects of ASP solver languages and often the amount of information a user has to deal with during debugging is high. In this work, we introduce stepping for ASP, a novel technique for debugging answer-set programs that can deal with current solver languages. It allows the user to follow his or her intuition on which rule instances to be active. This way, one can focus on interesting parts of the debugging search space from the beginning. Bugs are detected during stepping by revealing differences between the actual semantics of the program and the expectations of the user. As a solid formal basis for stepping, we develop a framework of computations for answer-set programs. For fully supporting solver languages we were faced with several challenges in doing so. For one, the languages of answer-set solvers differ from each other and from formal ASP languages in various ways. Thus, an abstract ASP language is needed that is sufficiently general to capture different solver languages. To this end, we make use of abstract constraints as an established abstraction for popular language constructs such as aggregates. None of the existing semantics for the targeted class of programs is compatible with all the solvers we want to support. Thus, we develop such a semantics and show several properties thereof. Moreover, we present different characterisations of the semantics that are relevant to stepping. Stepping has been implemented in SeaLion, an integrated development environment for ASP. We discuss the main features of SeaLion and explain our approach using example scenarios. Moreover, we elaborate on methodological aspects and the embedding of stepping in the ASP development process.