Advances of Proof Scores in CafeOBJ
arXiv:2112.10373 · doi:10.1016/j.scico.2022.102893
Abstract
Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification (i.e., to check whether a specification has desirable properties) is still one of the most important challenges in software/system engineering. CafeOBJ is an executable algebraic specification language system and domain/requirement/design engineers can write proof scores for improving quality of specifications by the specification verification. This paper describes advances of the proof scores for the specification verification in CafeOBJ.
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