论文标题
来自答案集编程规范的指针数据结构合成
Pointer Data Structure Synthesis from Answer Set Programming Specifications
论文作者
论文摘要
我们开发了一种归纳性验证技术，以从答案集编程（ASP）形式主义中表达的行为规格生成指针数据结构的命令程序。 ASP是一种基于非单调逻辑的形式主义，采用否定，有助于模仿人类的思维过程，使领域专家能够简洁地模拟所需的系统行为。我们在本文中争辩说，ASP依赖否定 - 与否定相比，它比基于撰写形式规格的一阶逻辑的形式主义更好。我们假设A域专家提供了归纳定义的数据结构以及其操作规范的表示。我们的程序与规格上的新颖校对理由相结合，并自动生成命令式程序。我们的校对技术利用部分推论的想法来简化逻辑规格。通过代数简化逻辑规格，我们得出了一个残留规范，可以将其解释为适当的命令程序。这项工作是在构建根据给定规范的正确程序的领域。
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.
