Principles of proof scores in CafeOBJ
Principles of proof scores in CafeOBJ
复制标题
DOI：
10.1016/j.tcs.2012.07.041
复制
发表时间：
2012-12
期刊：
影响因子：
--
通讯作者：
K. Futatsugi;Daniel Găină;K. Ogata
中科院分区：
文献类型：
--
作者：
K. Futatsugi;Daniel Găină;K. Ogata
本文描述了CafeOBJ代数规格说明语言中的证明分数验证方法的理论原理。验证方法以条件方程为中心，实现系统的定理证明（或交互式验证）。使用一个简单但有指导意义的例子来解释该方法，并且用精确的数学定义来描述证明验证的每一步的必要理论基础。给出了由这些定义所得到的一些重要定理。
This paper describes the theoretical principles of a verification method with proof scores in the CafeOBJ algebraic specification language. The verification method focuses on specifications with conditional equations and realizes systematic theorem proving (or interactive verification). The method is explained using a simple but instructive example, and the necessary theoretical foundations, which justify every step of the verification, are described with precise mathematical definitions. Some important theorems that result from the definitions are also presented.