HackerPapers

arXiv:2305.17485cs.LO

External Behavior of a Logic Program and Verification of Refactoring

Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, Nathan Temple

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

Abstract

Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.

arXiv comments
Accepted to Theory and Practice of Logic Programming (ICLP 2023)
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Sep 2024 to Sep 2024. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

  • Help Finding LLM and Proof Based Refactoring Reference1 point0 comments

    Recently on HN I came across an LLM paper achieving impressive results on SWE-bench refactoring tasks. In addition to generating the refactoring, it also created a formal proof of equivalence in a special DSL. Now I can't seem to find the paper! So far, I have scrubbed the HN SWE-bench articles from the last 9 months, and tried Google scholar searches for LLM based refactoring with Proofs or DSLs. I am confident that they mention SWE-bench in the abstract, but it does not seem to be mentioned…

Connected through shared HN threads, not inferred similarity or a recommendation.