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.
翻译:计算过程中意外的失败在软件开发中频繁发生且令人困扰。由外部原因(如文件缺失、权限不足)导致的失败可通过异常处理程序捕获。而编程失败(如以预期之外的参数调用部分定义的操作)常因假设软件正确而未被捕获。本文提出了一种验证此类假设的方法:首先推断操作的非失败条件,随后在部分定义操作的所有使用点进行验证。若验证通过,则可确保此类失败不会发生;若未通过,程序员可调整程序以处理可能的失败情形并再次验证。该方法完全自动化,适用于大规模声明式程序。最后,我们展示了在函数逻辑Curry程序上的实现结果。