Proving Partial Correctness and Termination of Mutually Recursive Programs

被引：0
|
作者：
Popov, Nikolaj [1 ]
Jebelean, Tudor [1 ]
机构：
[1] Johannes Kepler Univ Linz, Symbol Computat Res Inst, Linz, Austria
来源：
12TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2010) | 2011年
关键词：
D O I：
10.1109/SYNASC.2010.65
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present an environment for proving correctness of mutually recursive functional programs. As usual, correctness is transformed into a set of first-order predicate logic formulae-verification conditions. As a distinctive feature of our method, these formulae are not only sufficient, but also necessary for the correctness.
引用
收藏
页码：153 / 156
页数：4
相关论文
共 50 条
12345