Pointer Data Structure Synthesis from Answer Set Programming Specifications

TL;DR

This paper introduces a novel inductive proof-technique that automatically synthesizes imperative pointer data structure programs from behavioral specifications expressed in Answer Set Programming (ASP), leveraging logical simplification and partial deduction.

Contribution

It presents a new proof-technique that uses ASP specifications and algebraic simplification to automatically generate correct imperative programs for pointer data structures.

Findings

Successfully synthesizes pointer data structure programs from ASP specifications

Demonstrates the effectiveness of algebraic simplification in program synthesis

Provides a framework for reasoning over logical specifications to generate imperative code

Abstract

We develop an inductive proof-technique to generate imperative programs for pointer data structures from behavioural specifications expressed in the Answer Set Programming (ASP) formalism. ASP is a non-monotonic logic based formalism that employs negation-as-failure which helps emulate the human thought process, allowing domain experts to model desired system behaviour succinctly. We argue in this paper that ASP's reliance on negation-as-failure makes it a better formalism than those based on first-order logic for writing formal specifications. We assume the a domain expert provides the representation of inductively defined data structures along with a specification of its operations. Our procedures combined with our novel proof-technique reason over the specifications and automatically generate an imperative program. Our proof-technique leverages the idea of partial deduction to simplify logical specifications. By algebraically simplifying logical specifications we arrive at a residual specification which can be interpreted as an appropriate imperative program. This work is in the realm of constructing programs that are correct according to a given specification.