Advances of Proof Scores in CafeOBJ
This work targets domain, requirement, and design engineers in software/system engineering, but appears incremental as it builds on existing methods in CafeOBJ.
The paper addresses the challenge of specification verification in software/system engineering by advancing proof scores in CafeOBJ, aiming to improve the quality of specifications through verification, though no concrete results or numbers are provided.
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.