Automated Generation of C and NET Code Contracts from VDM SL Models
Automatic code generation gives software engineers a convenient way to realise a VDM SL specification in a programming language in order to achieve interoperability with standard libraries and external software modules. This paper presents a set of rules for translating VDM SL to C# The rules have been implemented in a proof of concept transcompiler as an extension to the Overture tool. The performances of the .NET Code Contracts library and the OpenJML tool are measured and compared, revealing a significant computational overhead in the latter.