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.

翻译：在领域、需求和/或设计规约层面仍然存在关键缺陷，规约验证（即检查规约是否具有理想属性）仍是软件/系统工程中最重要的挑战之一。CafeOBJ是一种可执行代数规约语言系统，领域/需求/设计工程师可编写证明分数，通过规约验证提升规约质量。本文阐述了CafeOBJ中用于规约验证的证明分数的进展。