A formal approach to object-oriented software engineering

被引：7
|
作者：
Wirsing, M [1 ]
Knapp, A [1 ]
机构：
[1] Univ Munich, Inst Informat, D-80538 Munich, Germany
来源：
THEORETICAL COMPUTER SCIENCE | 2002年 / 285卷 / 02期
关键词：
integrated formal software engineering; OOSE; rewriting logic; Maude; reflection; process algebra;
D O I：
10.1016/S0304-3975(01)00367-X
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We show how formal specifications can be integrated into one of the current pragmatic object-oriented software development methods. Jacobson's "object-oriented software engineering" process is combined with object-oriented algebraic specifications by extending object and interaction diagrams with formal annotations. The specifications are based on Meseguer's rewriting logic and are written in a meta-level extension of the language Maude by process expressions. As a result any such diagram can be associated with a formal specification, proof obligations ensuring invariant properties can be automatically generated, and the refinement relations between documents at different abstraction levels can be formally stated and proved. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：519 / 560
页数：42
相关论文
共 50 条
12345