Programmers may be hesitant to use declarative systems, because of the associated learning curve. In this paper, we present an API that integrates the IDP Knowledge Base system into the Python programming language. IDP is a state-of-the-art logical system, which uses SAT, SMT, Logic Programming and Answer Set Programming technology. Python is currently one of the most widely used (teaching) languages for programming. The first goal of our API is to allow a Python programmer to use the declarative power of IDP, without needing to learn any new syntax or semantics. The second goal is allow IDP to be added to removed from an existing code base with minimal changes.
In @cite_7 , a reasoner for FO extended with transitive closure is integrated into Java. Their KB language is therefore very similar to (but more restricted than) that of IDP. When it comes to the integration in Java, there are two main differences to our approach. First, the declarative knowledge is not written in expressions in the host language, but in a separate language (the Alloy-like JFSL @cite_3 ). Second, the integration into Java is done in an object-oriented way: the programmer defines classes in which formulas are added as, among others, class invariants, method pre- postconditions and frame conditions. In comparison, our Python API seems more lightweight, since it does not require an object-oriented approach. When it comes to computational performance, @cite_7 reports good results, which our implementation is not able to match.
@cite_3 @cite_7
2115900163 2168617729
This thesis presents a new light-weight specification language called JForge Specification Language (JFSL) for object-oriented languages such as Java. The language is amenable to bounded verification analysis by a tool called JForge that interprets JFSL specifications, fully integrates with a mainstream development environment, and assists programmers in examining counter example traces and debugging specifications. JFSL attempts to address challenges of specification languages such as inheritance, frame conditions, dynamic dispatch, and method calls inside specifications in the context of bounded verification. A collection of verification tasks illustrates the expressiveness and conciseness of JForge specifications and demonstrates effectiveness of the bounded verification technique. Thesis Supervisor: Daniel N. Jackson Title: Professor We present a unified environment for running declarative specifications in the context of an imperative object-Oriented programming language. Specifications are Alloy-like, written in first-order relational logic with transitive closure, and the imperative language is Java. By being able to mix imperative code with executable declarative specifications, the user can easily express constraint problems in place, i.e., in terms of the existing data structures and objects on the heap. After a solution is found, the heap is updated to reflect the solution, so the user can continue to manipulate the program heap in the usual imperative way. We show that this approach is not only convenient, but, for certain problems can also outperform a standard imperative implementation. We also present an optimization technique that allowed us to run our tool on heaps with almost 2000 objects.