为声明式程序推断非失败条件
Inferring Non-Failure Conditions for Declarative Programs
AI总结:
本文提出一种全自动方法,通过推断并检查操作的非失败条件来验证声明式程序中部分定义操作调用的正确性,并在 Curry 程序中实现验证。
摘要:
软件开发过程中,计算期间的非预期失败令人痛苦但频繁发生。由外部原因(例如文件缺失、无权限)导致的失败可被异常处理器捕获。编程失败,例如使用非预期参数调用部分定义的操作,通常由于假设软件是正确的而未被捕获。本文提出一种验证此类假设的方法。为此,推断操作的非失败条件,然后在部分定义操作的所有使用处进行检查。在肯定情况下,可确保不存在此类失败。在否定情况下,程序员可以调整程序以处理可能失败的情形,并再次检查程序。我们的方法是全自动的,可应用于较大的声明式程序。本文给出了一个针对函数逻辑 Curry 程序的实现结果。
英文摘要:
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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。