Home   >   CSC-OpenAccess Library   >    Manuscript Information
A Tool Generating a C# Code with Contracts of Code Contracts from a VDM++ Model with Conditions
Yuma Yamano, Toshihiko Ando, Keishi Okamoto
Pages - 27 - 39     |    Revised - 30-09-2020     |    Published - 31-10-2020
Volume - 8   Issue - 3    |    Publication Date - October 2020  Table of Contents
MORE INFORMATION
KEYWORDS
Formal Methods, Code Generation, VDM++, C#, Code Contracts.
ABSTRACT
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.
1 Google Scholar 
2 refSeek 
3 Scribd 
"Overture Tool." Internet: overturetool.org, [Aug. 28, 2020].
D. Strauss. (2016, Mar. 18). C# Code Contracts Succinctly. [On-line]. Available: www.syncfusion.com/ebooks/csharpcontracts [Oct. 5, 2020].
D.R. Cok. "OpenJML: JML for Java 7 by Extending OpenJDK," in NASA Formal Methods, Lecture Notes in Computer Science, vol. 6617, pp. 472-479. M. Bobaru, K. Havelund, G.J. Holzmann and R. Joshi, Ed. Berlin Heidelberg: Springer, 2011, pp. 472-479.
Galois inc. "SAW - tutorial." Internet: saw.galois.com/tutorial.html, [Aug. 28, 2020].
GitHub. "dotnet/Roslyn." Internet: github.com/dotnet/roslyn, [Aug. 28, 2020].
J. Fitzgerald, P.G. Larsen. Modelling Systems - Practical Tools and Techniques in Software Development. Cambridge: Cambridge University Press, 2009, pp. 1-228.
J.R. Abrial. Modeling in Event-B: system and software engineering. Cambridge: Cambridge University Press, 2010, pp. 1-586.
K. Claessen and J. Hughes. "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs," in Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, 2000, pp. 268-279.
K.R.M. Leino, "Dafny: An automatic program verifier for functional correctness." in Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol. 6355. E.M. Clarke, A. Voronkov, Ed. Berlin, Heidelberg: Springer, 2010, pp. 348-370.
Kyushu University. "FM VDM", Internet: fmvdm.org/, [Aug. 28, 2020].
Kyushu University. "VDMTools User Manual." Internet: github.com/vdmtools/vdmtools/raw/stable/doc/user-man/usermanpp_a4E.pdf, [Oct. 5, 2020]
M. Barnett, K.R.M. Leino and W. Schulte. "The Spec# Programming System: An Overview," in Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2004. Lecture Notes in Computer Science, vol. 3362. G. Barthe, L. Burdy, M. Huisman, JL. Lanet JL and T. Muntean, Ed. Berlin, Heidelberg: Springer, 2005, pp. 49-69.
M. Dalvandi, M. Butler and A. Rezazadeh. "From Event-B Models to Dafny Code Contracts," in 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015), 2015, pp. 308-315.
Microsoft Research. "Code Contracts." Internet: research.microsoft.com/en- us/projects/contracts/, [Aug. 28, 2020].
Microsoft. "C# reference." Internet: docs.microsoft.com/en-us/dotnet/csharp/language- reference/, Feb. 14, 2017 [Oct. 5, 2020].
N. Battle. "VDMJ." Internet: github.com/nickbattle/vdmj, [Aug. 28, 2020].
P.G. Larsen, K. Lausdahl, N. Battle, J. Fitzgerald, S. Wolff, S. Sahara, M. Verhoef, P.W.V. TranJ�rgensen, T. Oda, P. Chisholm. "VDM-10 Language Manual." Internet: overturetool.org/documentation/manuals.html [Oct. 5, 2020].
P.W.V. Tran-Jørgensen, P.G. Larsen and G.T. Leavens. "Automated translation of VDM to JML-annotated Java." International Journal on Software Tools for Technology Transfer, volume 20, pp. 211-235, Apr. 2018.
S. Agerholm, P.G. Larsen. "A Lightweight Approach to Formal Methods," in Applied Formal Methods - FM-Trends 98. FM-Trends 1998. Lecture Notes in Computer Science, vol. 1641. 1999, pp. 168-183.
S. Diswal, P.W.V. Tran-Jørgensen and P.G. Larsen. "Automated Generation of C# and .NET Code Contracts from VDM-SL Models," in THE 14TH OVERTURE WORKSHOP, 2016, pp. 32-47.
T. Kurita, F. Ishikawa and K. Araki. "Practices for Formal Models as Documents: Evolution of VDM Application to Mobile FeliCa IC Chip Firmware," in Formal Methods - 20th International Symposium, 2015, pp. 593-596.
V. Rivera, N. Catano, T. Wahls and C. Rueda. "Code generation for Event-B." International Journal on Software Tools for Technology Transfer, vol.19, pp.31-52, Feb. 2017.
Y. Chisaka and K. Okamoto. "A prototype of a translation tool from VDM++ to C#," in Proceedings of the 78th National Convention of IPSJ. 2016, pp.363-364.
Mr. Yuma Yamano
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan
a1811531@sendai-nct.jp
Dr. Toshihiko Ando
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan
Dr. Keishi Okamoto
Department of Information Systems, National Institute of Technology, Sendai College, Sendai, 989-3128 - Japan


CREATE AUTHOR ACCOUNT
 
LAUNCH YOUR SPECIAL ISSUE
View all special issues >>
 
PUBLICATION VIDEOS