A Tool Generating a C# Code with Contracts of Code Contracts from a VDM++ Model with Conditions

As systems rely on software, the reliability of the software is required. Formal methods are prominent ways to improve the reliability of software. Formal specification is one of the formal methods and offers a formal specification language based on mathematics and computer science. With this method, the ambiguity of the specification can be decreased, and verification can be facilitated. In development based on formal specification, specifications are formally described and then a code is generated from it. This generation is done manually in some cases, but it is done automatically by a tool in some cases. Generally, from the viewpoint of execution efficiency, etc., the generated code is modified, so it is necessary to verify whether the code meets the conditions in the specification. However, this task is manual in many cases, then it is time-consuming and error-prone. In this paper, we introduce a tool to generate a code in the programing language C# from a specification in the formal specification language VDM++. The tool also translates conditions of a specification into contracts of the library Code Contracts of #C. The above problem will be solved with this tool.