Issue |
Wuhan Univ. J. Nat. Sci.
Volume 26, Number 6, December 2021
|
|
---|---|---|
Page(s) | 481 - 488 | |
DOI | https://doi.org/10.1051/wujns/2021266481 | |
Published online | 17 December 2021 |
Computer Science
CLC number: TP305
A Method to Deduce and Synthesize the Dafny Programs
1
College of Computer Information Engineering, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
2
Management Science and Engineering Research Center, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
3
College of Physics and Communication Electronics, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
† To whom correspondence should be addressed. E-mail: zhengkang2005@iscas.ac.cn
Received:
16
October
2021
We propose a systematic method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems, and so on. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble Sorting program.
Key words: Dafny / deductive synthesis / specification transformation technology / recursive relationships / loop invariants
Biography: WANG Changjing, male, Ph. D., Professor, research direction: software formal method, trustworthy software. E-mail: wcj771006@163.com
Foundation item: Supported by the National Natural Science Foundation of China (61762049, 61862033, 61902162 ,11804133) and Natural Science Foundation of Jiangxi Province (20202BABL202025, 20202BABL202026, 20202BAB202015)
© Wuhan University 2021
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.