2020/06/12 by Sarat Chandra Varanasi, Varanasi, Sarat Chandra, Neeraj Mittal +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation #Symbolic Computation (cs.SC)
paper · pdf · doi:10.48550/arxiv.2006.07440
openalex publication_date 2020/06/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We develop an inductive proof-technique to generate imperative programs for\npointer data structures from behavioural specifications expressed in the Answer\nSet Programming (ASP) formalism. ASP is a non-monotonic logic based formalism\nthat employs negation-as-failure which helps emulate the human thought process,\nallowing domain experts to model desired system behaviour succinctly. We argue\nin this paper that ASP's reliance on negation-as-failure makes it a better\nformalism than those based on first-order logic for writing formal\nspecifications. We assume the a domain expert provides the representation of\ninductively defined data structures along with a specification of its\noperations. Our procedures combined with our novel proof-technique reason over\nthe specifications and automatically generate an imperative program. Our\nproof-technique leverages the idea of partial deduction to simplify logical\nspecifications. By algebraically simplifying logical specifications we arrive\nat a residual specification which can be interpreted as an appropriate\nimperative program. This work is in the realm of constructing programs that are\ncorrect according to a given specification.\n