TY - GEN
T1 - Refactoring formal specifications in object-Z
AU - Hui, Liu
AU - Bin, Zhu
PY - 2008
Y1 - 2008
N2 - Software refactoring is to restructure artifacts to improve software quality, especially readability, extensibility, and maintainability, while preserving its external behaviors. Software refactoring has been successfully applied to source code and design models. However, refactoring has not yet been introduced to formal specifications. Compared to source code in programming languages similar to nature languages, formal specifications in formal mathematic languages are in urgent need of refactoring because mathematic languages are usually more difficult to understand or modify. Furthermore, formal specifications' inherent formality makes it easier to validate behavior preservation of refactorings, which dramatically increases the dependability of refactorings. This paper illustrates the necessity and possibility of refactoring formal specifications. It first illustrates the necessity with an motivating example, and then proposes a series of primitive refactorings and advanced refactorings that are composed of primitive refactorings.
AB - Software refactoring is to restructure artifacts to improve software quality, especially readability, extensibility, and maintainability, while preserving its external behaviors. Software refactoring has been successfully applied to source code and design models. However, refactoring has not yet been introduced to formal specifications. Compared to source code in programming languages similar to nature languages, formal specifications in formal mathematic languages are in urgent need of refactoring because mathematic languages are usually more difficult to understand or modify. Furthermore, formal specifications' inherent formality makes it easier to validate behavior preservation of refactorings, which dramatically increases the dependability of refactorings. This paper illustrates the necessity and possibility of refactoring formal specifications. It first illustrates the necessity with an motivating example, and then proposes a series of primitive refactorings and advanced refactorings that are composed of primitive refactorings.
KW - Formal specifications
KW - Object-Z
KW - Software refactoring
KW - Z
UR - https://www.scopus.com/pages/publications/79951496075
U2 - 10.1109/CSSE.2008.260
DO - 10.1109/CSSE.2008.260
M3 - Conference contribution
AN - SCOPUS:79951496075
SN - 9780769533360
T3 - Proceedings - International Conference on Computer Science and Software Engineering, CSSE 2008
SP - 342
EP - 345
BT - Proceedings - International Conference on Computer Science and Software Engineering, CSSE 2008
T2 - International Conference on Computer Science and Software Engineering, CSSE 2008
Y2 - 12 December 2008 through 14 December 2008
ER -