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 transfo...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.展开更多
基金Supported by the National Natural Science Foundation of China(61762049,61862033,61902162,11804133)Natural Science Foundation of Jiangxi Province(20202BABL202025,20202BABL202026,20202BAB202015)。
文摘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.
