• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and practice of logic programming >Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
【24h】

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

机译：Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相关主题

摘要

We address the problem of verifying that the functions of a program meet their contracts, specifiedby pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs)by which the verification problem is reduced to the problem of checking satisfiability of a set ofclauses derived from the given program and contracts. We consider programs that manipulatealgebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functionsdefined by simple recursion schemata on the given ADTs. We show by several examplesthat state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problemsobtained by direct translation of the contracts into CHCs. To overcome this difficulty, wepropose a transformation technique that removes the ADT terms from CHCs and derives newsets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using thederived CHCs there is no need for induction rules on ADTs. We prove that the transformation issound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also provethat the transformation always terminates for the class of contracts specified by catamorphisms.Finally, we present the experimental results obtained by an implementation of our techniquewhen verifying many non-trivial contracts for ADT manipulating programs.

著录项

获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号