Using OCL for verified re-engineering

Since 2021 we have been using UML and OCL to represent the semantics of software systems undergoing re-engineering, to facilitate translation of legacy systems to functionally-equivalent versions in a new platform or software language. In this paper we assess the lessons learnt from this approach, particularly as regards the appropriateness of OCL to represent software semantics. We identify areas where natural extensions of OCL would be useful to represent program semantics, and indicate how these extensions can be incorporated into the OCL standard.