结合静态和动态契约检查的Curry算法
Combining Static and Dynamic Contract Checking for Curry
摘要：
静态类型系统通常不足以表达对函数调用的所有要求。因此，带有前置和后置条件的契约可以用来表达对操作的更复杂的约束。可以在运行时间检查协定，以确保仅使用合理的参数调用操作并返回预期的结果。虽然这种动态契约检查提供了更可靠的程序执行，但它需要执行时间，并可能导致程序崩溃，这些崩溃可能会在编译时用更高级的方法检测到。为了改善这种情况的声明性语言，我们提出了一种方法，结合静态和动态的合同检查的功能逻辑语言咖喱。基于函数式逻辑程序设计中契约检验的形式化模型，提出了一种在编译时自动检验契约的方法。如果合同验证成功，则可以省略对合同的动态检查。这种方法减少了执行时间，而不会降低可靠的程序执行。在最好的情况下，当所有契约都被静态验证时，它提供了对软件的信任，因为在程序执行期间不会发生由于违反契约而导致的崩溃。
英文摘要：
Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, dynamic checking of it can be omitted. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
