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规格核查的证明分数的进展。