论文部分内容阅读
UML2．0OCL是基于一阶谓词逻辑和集合论的形式化语言，用它对UML类图进行条件约束后，类图便具备了严格的语法和精确的语义，同时也具备了演绎验证的基本条件．但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证，因此提出了将带OCL约束的UML类图通过Object—Z进行形式化描述的方法，这样便可以充分利用Object—Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等。