CafeOBJ 中证明分数的进展
软件工程
2023-12-07 v3 计算机科学中的逻辑
摘要
在领域、需求和/或设计规约层面，关键缺陷持续存在，而规约验证（即检查规约是否具有期望性质）仍是软件/系统工程中最重要的挑战之一。CafeOBJ 是一个可执行的代数规约语言系统，领域/需求/设计工程师可以编写证明分数，通过规约验证来提高规约质量。本文描述了 CafeOBJ 中用于规约验证的证明分数的进展。
引用
@article{arxiv.2112.10373,
title = {Advances of Proof Scores in CafeOBJ},
author = {Kokichi Futatsugi},
journal= {arXiv preprint arXiv:2112.10373},
year = {2023}
}
备注
59 pages, Appendix A is newly added, Subsection 5.4 is significantly revised and extended, some notations are changed to make them consistent with others, and several parts are revised to improve readability