This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative – they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.

Our example shows how dealing with “logic” and with “control” can be separated. Most of the proofs can be done at the “logic” level, abstracting from any operational semantics.

The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.

We introduce a stepping methodology for answer-set programming (ASP) that allows for debugging answer-set programs and is based on the stepwise application of rules. Similar to debugging in imperative languages, where the behaviour of a program is observed during a step-by-step execution, stepping for ASP allows for observing the effects that rule applications have in the computation of an answer set. While the approach is inspired from debugging in imperative programming, it is conceptually different to stepping in other paradigms due to non-determinism and declarativity that are inherent to ASP. In particular, unlike statements in an imperative program that are executed following a strict control flow, there is no predetermined order in which to consider rules in ASP during a computation. In our approach, the user is free to decide which rule to consider active in the next step following his or her intuition. This way, one can focus on interesting parts of the debugging search space. 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 different solver languages, we build our framework on an abstract ASP language 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. Stepping has been implemented in SeaLion, an integrated development environment for ASP. We illustrate stepping using an example scenario and discuss the stepping plugin of SeaLion. Moreover, we elaborate on methodological aspects and the embedding of stepping in the ASP development process.

In Constraint Programming, a portfolio solver combines a variety of different constraint solvers for solving a given problem. This fairly recent approach enables to significantly boost the performance of single solvers, especially when multicore architectures are exploited. In this work, we give a brief overview of the portfolio solver sunny-cp, and we discuss its performance in the MiniZinc Challenge—the annual international competition for Constraint Programming solvers—where it won two gold medals in 2015 and 2016.

A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques automating this labour-intensive process. A prominent example is the successful use of randomness, in particular, random typable λ-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable λ-terms, no effective uniform sampling method is known, setting it as a fundamental open problem in the random software testing approach. In this paper, we combine the framework of Boltzmann samplers, a powerful technique of random combinatorial structure generation, with today's Prolog systems offering a synergy between logic variables, unification with occurs check and efficient backtracking. This allows us to develop a novel sampling mechanism able to construct uniformly random closed simply typed λ-terms of up size 120. We apply our techniques to the generation of uniformly random closed simply typed normal forms and design a parallel execution mechanism pushing forward the achievable term size to 140.

Algorithm 4 on page 960 of the above named article (Wielemaker and Harris 2016) is flawed. The issue is illustrated by algorithm 1 (supplementary figure 1). If a thread A detects the condition table too full is false it proceeds adding its atom to the table. If thread B detects the table is (now) too full it starts a resize. The resize allocates a new table and copies the atoms from the old to the new table. If thread A adds the new atom after the copy loop passes its location and before thread B activates the new table the insertion is considered successful, but the new atom is only in the deactivated old table.

The links to the online only Technical Communications in Lamma and Swift (2013) are unfortunately broken. All of the Technical Communications can be found here:

https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/editorial-29th-international-conference-on-logic-programming-special-issue/82FDD81073DC30A563ED242516CADAAE#fndtn-supplementary-materials