Alloy as a Refactoring Checker?

被引：5

作者：

Estler, H. -Christian ^{[1
]}

Wehrheim, Heike ^{[1
]}

机构：

[1] Univ Paderborn, Inst Informat, D-33098 Paderborn, Germany

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 214卷

关键词：

Alloy; refactoring; refinement; behaviour preservation; Z;

D O I：

10.1016/j.entcs.2008.06.015

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Refactorings are systematic changes made to programs, models or specifications in order to improve their structure without changing the externally observable behaviour. We will examine how a constraint solver (the Alloy Analyzer) can be used to automatically check if refactorings, applied to a formal specification (written in Z), meet this requirement. Furthermore, we identify a class of refactorings for which the use of this tool is reasonable in general.

引用

页码：331 / 357

页数：27

共 20 条

[1] Using the Alloy Analyzer to Verify Data Refinement in Z [J].

Bolton, Christie .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 137 (02) :23-44

[2]

de Moura L, 2004, LECT NOTES COMPUT SC, V3114, P496

[3]

DEROEVER WP, 1999, DATA REFINEMENT MODE

[4]

Derrick J., 2001, FACIT

[5] Modelchecking Correctness of Refactorings - Some Experiments [J].

Estler, H. Christian ;

Ruhroth, Thomas ;

Wehrheim, Heike .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 187 (3-17) :3-17

[6]

Fowler Martin, 1999, REFACTORING IMPROVIN

[7] Alloy: A lightweight object modelling notation [J].

Jackson, D .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2002, 11 (02) :256-290

[8]

Jackson D., 2006, SOFTWARE ABSTRACTION

[9]

Jackson Daniel, 2000, ACM SIGSOFT S FDN SO, V25, DOI [10.1145/357474.355063, DOI 10.1145/357474.355063]

[10]

Johnson R. E., 1990, P SOOPPA 90 S OBJ OR

← 1 2 →