Advances of Proof Scores in CafeOBJ : Invited Paper

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 in CafeOBJ for improving quality of specifications by the specification verification. This paper describes advances of the proof scores for the specification verification in CafeOBJ from the author’s point of view.