nach oben

2022 | Buch

Kapitel lesen Erstes Kapitel lesen

Logic-Based Program Synthesis and Transformation

31st International Symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021, Proceedings

herausgegeben von: Emanuele De Angelis, Prof. Wim Vanhoof

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 31st International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2021, which was held during September 7-8, 2021.*

The 8 papers presented in this volume were carefully reviewed and selected from a total of 15 reviewed submissions. Additionally, the book also contains 1 full-length invited talk.

*Conference was held as a hybrid event due to the COVID-19 pandemic.

Inhaltsverzeichnis

Frontmatter

String Abstract Domains and Their Combination

Abstract

We survey recent developments in string static analysis, with an emphasis on how string abstract domains can be combined. The paper has formed the basis for an invited presentation given to LOPSTR 2021 and PPDP 2021.

Harald Søndergaard

Data Type Inference for Logic Programming

Abstract

In this paper we present a new static data type inference algorithm for logic programming. Without the need for declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases, correspond to the data types processed by their intended meaning. The algorithm is also able to infer types given data type definitions similar to data definitions in Haskell and, in this case, the inferred types are more informative, in general. We present the type inference algorithm, prove it is decidable and sound with respect to a type system, and, finally, we evaluate our approach on example programs that deal with different data structures.

João Barbosa, Mário Florido, Vítor Santos Costa

Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines

Abstract

The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists of two well-known program transformations: translation to continuation-passing style that uncovers the control flow of the evaluator and Reynolds’s defunctionalization that generates a first-order transition function. Ever since the transformation was first described by Danvy et al. it has found numerous applications in connecting known evaluators and abstract machines, but also in discovering new abstract machines for a variety of \(\lambda \)-calculi as well as for logic-programming, imperative and object-oriented languages.

We present an algorithm that automates the functional correspondence. The algorithm accepts an evaluator written in a dedicated minimal functional meta-language and it first transforms it to administrative normal form, which facilitates program analysis, before performing selective translation to continuation-passing style, and selective defunctionalization. The two selective transformations are driven by a control-flow analysis that is computed by an abstract interpreter obtained using the abstracting abstract machines methodology, which makes it possible to transform only the desired parts of the evaluator. The article is accompanied by an implementation of the algorithm in the form of a command-line tool that allows for automatic transformation of an evaluator embedded in a Racket source file and gives fine-grained control over the resulting machine.

Maciej Buszka, Dariusz Biernacki

S-Semantics–an Example

Abstract

The s-semantics makes it possible to explicitly deal with variables in program answers. So it seems suitable for programs using nonground data structures, like open lists. However it is difficult to find published examples of using the s-semantics to reason about particular programs.

Here we apply s-semantics to prove correctness and completeness of Frühwirth’s n queens program. This is compared with a proof, published elsewhere, based on the standard semantics and Herbrand interpretations.

Włodzimierz Drabent

Disjunctive Delimited Control

Abstract

Delimited control is a powerful mechanism for programming language extension which has been recently proposed for Prolog (and implemented in SWI-Prolog). By manipulating the control flow of a program from inside the language, it enables the implementation of powerful features, such as tabling, without modifying the internals of the Prolog engine. However, its current formulation is inadequate: it does not capture Prolog’s unique non-deterministic nature which allows multiple ways to satisfy a goal.

This paper fully embraces Prolog’s non-determinism with a novel interface for disjunctive delimited control, which gives the programmer not only control over the sequential (conjunctive) control flow, but also over the non-deterministic control flow. We provide a meta-interpreter that conservatively extends Prolog with delimited control and show that it enables a range of typical Prolog features and extensions, now at the library level: findall, cut, branch-and-bound optimisation, probabilistic programming, ...

Alexander Vandenbroucke, Tom Schrijvers

Towards Substructural Property-Based Testing

Abstract

We propose to extend property-based testing to substructural logics to overcome the current lack of reasoning tools in the field. We take the first step by implementing a property-based testing system for specifications written in the linear logic programming language Lolli. We employ the foundational proof certificates architecture to model various data generation strategies. We validate our approach by encoding a model of a simple imperative programming language and its compilation and by testing its meta-theory via mutation analysis.

Marco Mantovani, Alberto Momigliano

The Next 700 Program Transformers

Abstract

In this paper, we describe a hierarchy of program transformers, capable of performing fusion to eliminate intermediate data structures, in which the transformer at each level of the hierarchy builds on top of those at lower levels. The program transformer at level 1 of the hierarchy corresponds to positive supercompilation, and that at level 2 corresponds to distillation. We give a number of examples of the application of our transformers at different levels in the hierarchy and look at the speedups that are obtained. We determine the maximum speedups that can be obtained at each level, and prove that the transformers at each level terminate.

Geoff Hamilton

Representation and Processing of Instantaneous and Durative Temporal Phenomena

Abstract

Event definitions in Complex Event Processing systems are constrained by the expressiveness of each system’s language. Some systems allow the definition of instantaneous complex events, while others allow the definition of durative complex events. While there are exceptions that offer both options, they often lack of intervals relations such as those specified by the Allen’s interval algebra. In this paper, we propose a new logic based temporal phenomena definition language, specifically tailored for Complex Event Processing. Our proposed language allows the representation of both instantaneous and durative phenomena and the temporal relations between them. Moreover, we demonstrate the expressiveness of our proposed language by employing a maritime use case where we define maritime events of interest. We analyse the execution semantics of our proposed language for stream processing and finally, we introduce and evaluate on real world data, Phenesthe, our open-source Complex Event Processing system.

Manolis Pitsikalis, Alexei Lisitsa, Shan Luo

Prefix-Based Tracing in Message-Passing Concurrency

Abstract

The execution of concurrent applications typically involves some degree of nondeterminism, mostly due to the relative speeds of concurrent processes. An essential task in state-space exploration techniques for the verification of concurrent programs consists in finding points in an execution where alternative actions are possible. Here, the nondeterministic executions of a program can be represented by a tree-like structure. Given the trace of a concrete execution, one first identifies its branching points. Then, a new execution can be steered up to one of these branching points (using, e.g., a partial trace), so that an unexplored branch can be considered. From this point on, the execution proceeds nondeterministically, eventually producing a trace of the complete execution as a side-effect, and the process starts again. In this paper, we formalize this operation—partially driving the execution of a program and then producing a trace of the entire execution—, which we call prefix-based tracing. It combines ideas from both record-and-replay debugging and execution tracing. We introduce a semantics-based formalization of prefix-based tracing in the context of a message-passing concurrent language like Erlang. Furthermore, we also present an implementation of prefix-based tracing by means of a program instrumentation.

Juan José González-Abril, Germán Vidal

Backmatter

Titel: Logic-Based Program Synthesis and Transformation
herausgegeben von: Emanuele De Angelis
Prof. Wim Vanhoof
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-98869-2
Print ISBN: 978-3-030-98868-5
DOI: https://doi.org/10.1007/978-3-030-98869-2