@Article{Jorgensen&17,
author="Tran-J{\o}rgensen, Peter W. V.
and Larsen, Peter Gorm
and Leavens, Gary T.",
title="{Automated translation of VDM to JML-annotated Java}",
journal="International Journal on Software Tools for Technology Transfer",
year="2017",
pages="1--25",
abstract="When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-based elements such as invariants and pre- and postconditions into account during the code-generation process. The contract-based elements of the Vienna Development Method Specification Language (VDM-SL) are translated into corresponding constructs in the Java Modelling Language (JML) and used to validate the generated code against the properties of the VDM model. VDM-SL and JML are both Design-by-Contract (DbC) languages, with the difference that VDM-SL supports abstract modelling and system specification, while JML is used for detailed specification of Java classes and interfaces. We describe the semantic differences between the contract-based elements of VDM-SL and JML and formulate the translation as a set of rules. We further demonstrate how dynamic JML assertion checks can be used to ensure the consistency of VDM's subtypes when a model is code-generated. The translator is fully automated and produces JML-annotated Java programs that can be checked for correctness using JML tools.",
issn="1433-2787",
doi="10.1007/s10009-017-0448-3",
url="http://dx.doi.org/10.1007/s10009-017-0448-3"
}

%G VDM TOOL OVERTURE

{"_id":"S2y9E3FJzmzQod3gk","bibbaseid":"tranjrgensen-larsen-leavens-automatedtranslationofvdmtojmlannotatedjava-2017","author_short":["Tran-Jørgensen, P. W. V.","Larsen, P. G.","Leavens, G. T."],"bibdata":{"bibtype":"article","type":"article","author":[{"propositions":[],"lastnames":["Tran-Jørgensen"],"firstnames":["Peter","W.","V."],"suffixes":[]},{"propositions":[],"lastnames":["Larsen"],"firstnames":["Peter","Gorm"],"suffixes":[]},{"propositions":[],"lastnames":["Leavens"],"firstnames":["Gary","T."],"suffixes":[]}],"title":"Automated translation of VDM to JML-annotated Java","journal":"International Journal on Software Tools for Technology Transfer","year":"2017","pages":"1–25","abstract":"When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-based elements such as invariants and pre- and postconditions into account during the code-generation process. The contract-based elements of the Vienna Development Method Specification Language (VDM-SL) are translated into corresponding constructs in the Java Modelling Language (JML) and used to validate the generated code against the properties of the VDM model. VDM-SL and JML are both Design-by-Contract (DbC) languages, with the difference that VDM-SL supports abstract modelling and system specification, while JML is used for detailed specification of Java classes and interfaces. We describe the semantic differences between the contract-based elements of VDM-SL and JML and formulate the translation as a set of rules. We further demonstrate how dynamic JML assertion checks can be used to ensure the consistency of VDM's subtypes when a model is code-generated. The translator is fully automated and produces JML-annotated Java programs that can be checked for correctness using JML tools.","issn":"1433-2787","doi":"10.1007/s10009-017-0448-3","url":"http://dx.doi.org/10.1007/s10009-017-0448-3","bibtex":"@Article{Jorgensen&17,\nauthor=\"Tran-J{\\o}rgensen, Peter W. V.\nand Larsen, Peter Gorm\nand Leavens, Gary T.\",\ntitle=\"{Automated translation of VDM to JML-annotated Java}\",\njournal=\"International Journal on Software Tools for Technology Transfer\",\nyear=\"2017\",\npages=\"1--25\",\nabstract=\"When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-based elements such as invariants and pre- and postconditions into account during the code-generation process. The contract-based elements of the Vienna Development Method Specification Language (VDM-SL) are translated into corresponding constructs in the Java Modelling Language (JML) and used to validate the generated code against the properties of the VDM model. VDM-SL and JML are both Design-by-Contract (DbC) languages, with the difference that VDM-SL supports abstract modelling and system specification, while JML is used for detailed specification of Java classes and interfaces. We describe the semantic differences between the contract-based elements of VDM-SL and JML and formulate the translation as a set of rules. We further demonstrate how dynamic JML assertion checks can be used to ensure the consistency of VDM's subtypes when a model is code-generated. The translator is fully automated and produces JML-annotated Java programs that can be checked for correctness using JML tools.\",\nissn=\"1433-2787\",\ndoi=\"10.1007/s10009-017-0448-3\",\nurl=\"http://dx.doi.org/10.1007/s10009-017-0448-3\"\n}\n\n%G VDM TOOL OVERTURE\n","author_short":["Tran-Jørgensen, P. W. V.","Larsen, P. G.","Leavens, G. T."],"key":"Jorgensen&17","id":"Jorgensen&17","bibbaseid":"tranjrgensen-larsen-leavens-automatedtranslationofvdmtojmlannotatedjava-2017","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/s10009-017-0448-3"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"https://www.overturetool.org/publications/overtureweb.bib","dataSources":["o4zfqwm7cQsSnyzzT","Crono4ygz53Pqi6FB","nGw4dfQFrDZqKC8vj"],"keywords":[],"search_terms":["automated","translation","vdm","jml","annotated","java","tran-jørgensen","larsen","leavens"],"title":"Automated translation of VDM to JML-annotated Java","year":2017}