Inferring Non-Failure Conditions for Declarative Programs

• URL: http://arxiv.org/abs/2402.12960v1
• Date: Tue, 20 Feb 2024 12:25:36 GMT
• Title: Inferring Non-Failure Conditions for Declarative Programs
• Authors: Michael Hanus
• Abstract summary: Unintended failures during a computation are painful but frequent during software development. Programming failures, such as calling a partially defined operation with unintended arguments, are often not caught due to the assumption that the software is correct. This paper presents an approach to verify such assumptions.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Unintended failures during a computation are painful but frequent during software development. Failures due to external reasons (e.g., missing files, no permissions) can be caught by exception handlers. Programming failures, such as calling a partially defined operation with unintended arguments, are often not caught due to the assumption that the software is correct. This paper presents an approach to verify such assumptions. For this purpose, non-failure conditions for operations are inferred and then checked in all uses of partially defined operations. In the positive case, the absence of such failures is ensured. In the negative case, the programmer could adapt the program to handle possibly failing situations and check the program again. Our method is fully automatic and can be applied to larger declarative programs. The results of an implementation for functional logic Curry programs are presented.

Related papers

• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  Large language models (LLMs) of code are typically trained on the surface textual form of programs. We propose NExT, a method to teach LLMs to inspect the execution traces of programs and reason about their run-time behavior.
  arXiv  Detail & Related papers  (2024-04-23T01:46:32Z)
• Reproducing Failures in Fault Signatures [5.458524825360132]
  We generate fault signatures from the failure locations and the original source code to reproduce the faults in small programs. A fault signature aims to contain only sufficient statements that can reproduce the faults. Our evaluation on real-world bugs from Corebench, BugBench, and Manybugs shows that fault signatures can reproduce the fault for the original programs.
  arXiv  Detail & Related papers  (2023-09-20T02:14:38Z)
• On Feasibility of Declarative Diagnosis [0.0]
  We argue that useful ways of declarative diagnosis of logic programs exist, and should be usable in actual programming. This paper discusses their possibly main weaknesses and shows how to overcome them.
  arXiv  Detail & Related papers  (2023-08-30T08:56:19Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• System Predictor: Grounding Size Estimator for Logic Programs under Answer Set Semantics [0.5801044612920815]
  We present the system Predictor for estimating the grounding size of programs. We evaluate the impact of Predictor when used as a guide for rewritings produced by the answer set programming rewriting tools Projector and Lpopt.
  arXiv  Detail & Related papers  (2023-03-29T20:49:40Z)
• Execution Time Program Verification With Tight Bounds [6.36836017515443]
  This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs.
  arXiv  Detail & Related papers  (2022-10-20T09:02:13Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  We propose fault-aware neural code rankers that can predict the correctness of a sampled program without executing it. Our fault-aware rankers can significantly increase the pass@1 accuracy of various code generation models.
  arXiv  Detail & Related papers  (2022-06-04T22:01:05Z)
• Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
  We propose to let the model perform sampling during training and learn from both self-sampled fully-correct programs and partially-correct programs. We show that our use of self-sampled correct and partially-correct programs can benefit learning and help guide the sampling process. Our proposed method improves the pass@k performance by 3.1% to 12.3% compared to learning from a single reference program with MLE.
  arXiv  Detail & Related papers  (2022-05-28T03:31:07Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  Execution result--minimum Bayes risk decoding for program selection. We show that it improves the few-shot performance of pretrained code models on natural-language-to-code tasks.
  arXiv  Detail & Related papers  (2022-04-25T06:06:08Z)
• Static Prediction of Runtime Errors by Learning to Execute Programs with External Resource Descriptions [31.46148643917194]
  We introduce a real-world dataset and task for predicting runtime errors. We develop an interpreter-inspired architecture with an inductive bias towards mimicking program executions. We show that the model can also predict the location of the error, despite being trained only on labels indicating the presence/absence and kind of error.
  arXiv  Detail & Related papers  (2022-03-07T23:17:17Z)
• IReEn: Reverse-Engineering of Black-Box Functions via Iterative Neural Program Synthesis [70.61283188380689]
  We investigate the problem of revealing the functionality of a black-box agent. We do not rely on privileged information on the black box, but rather investigate the problem under a weaker assumption of having only access to inputs and outputs of the program. Our results show that the proposed approach outperforms the state-of-the-art on this challenge by finding an approximately functional equivalent program in 78% of cases.
  arXiv  Detail & Related papers  (2020-06-18T17:50:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.