期刊文献+
共找到1篇文章
< 1 >
每页显示 20 50 100
Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules 被引量:2
1
作者 WANG Changjing CAO Zhongxiong +3 位作者 YU Chuling WANG Changchang HUANG Qing ZUO Zhengkang 《Wuhan University Journal of Natural Sciences》 CAS CSCD 2023年第3期246-256,共11页
The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verification reliability and automation.To solve the above problems,this paper proposes a nonline... The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verification reliability and automation.To solve the above problems,this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan’s refinement rules.First,we use recursive definition technique to characterize the initial specification.The specification is then transformed into GCL(Guarded Command Language)programs using loop invariant derivation and Morgan’s refinement rules.Furthermore,VCG(Verification Condition Generator)is used in the GCL program to generate the verification condition automatically.The Isabelle theorem prover then validates the GCL program’s correctness.Finally,the GCL code generates a C++executable program automatically via the conversion system.The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example.This method addresses the problem that the construction process’s loop invariant is difficult to obtain and the refinement process is insufficiently detailed.At the same time,the method improves verification process automation and reduces the manual verification workload. 展开更多
关键词 program construction partition recursion Morgan's refinement rules loop invariant VCG Isabelle theorem prover
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部