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.展开更多
We investigate strong stability preserving(SSP)implicit-explicit(IMEX)methods for partitioned systems of differential equations with stiff and nonstiff subsystems.Conditions for order p and stage order q=p are derived...We investigate strong stability preserving(SSP)implicit-explicit(IMEX)methods for partitioned systems of differential equations with stiff and nonstiff subsystems.Conditions for order p and stage order q=p are derived,and characterization of SSP IMEX methods is provided following the recent work by Spijker.Stability properties of these methods with respect to the decoupled linear system with a complex parameter,and a coupled linear system with real parameters are also investigated.Examples of methods up to the order p=4 and stage order q—p are provided.Numerical examples on six partitioned test systems confirm that the derived methods achieve the expected order of convergence for large range of stepsizes of integration,and they are also suitable for preserving the accuracy in the stiff limit or preserving the positivity of the numerical solution for large stepsizes.展开更多
Regularized Boolean operations have been widely used in 3D modeling systems. However, evaluating Boolean operations may be quite numerically unstable and time consuming, especially for iterated set operations. A novel...Regularized Boolean operations have been widely used in 3D modeling systems. However, evaluating Boolean operations may be quite numerically unstable and time consuming, especially for iterated set operations. A novel and unified technique is proposed in this paper for computing single and iterated set operations efficiently, robustly and exactly. An adaptive octree is combined with a nested constructive solid geometry （CSG） tree by this technique. The intersection handling is restricted to the cells in the octree where intersection actually occurs. Within those cells, a CSG tree template is instanced by the surfaces and the tree is converted to planebased binary space partitioning （BSP） for set evaluation; Moreover, the surface classification is restricted to the ceils in the octree where the surfaces only come from a model and are within the bounding-boxes of other polyhedrons. These two ways bring about the efficiency and scalability of the operations, in terms of runtime and memory. As all surfaces in such a cell have the same classification relation, they are classified as a whole. Robustness and exactness are achieved by integrating plane-based geometry representation with adaptive geometry predicate technique in intersection handling, and by applying divide-and-conquer arithmetic on surface classification. Experimental results demonstrate that the proposed approach can guarantee the robustness of Boolean computations and runs faster than other existing approaches.展开更多
基金Supported by the National Natural Science Foundation of China(62262031)Science and Technology Key Project of Education Department of Jiangxi Province(GJJ2200302,GJJ210307)the Graduate Innovative Special Fund Projects of Jiangxi Province(YJS2022064)
文摘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.
文摘We investigate strong stability preserving(SSP)implicit-explicit(IMEX)methods for partitioned systems of differential equations with stiff and nonstiff subsystems.Conditions for order p and stage order q=p are derived,and characterization of SSP IMEX methods is provided following the recent work by Spijker.Stability properties of these methods with respect to the decoupled linear system with a complex parameter,and a coupled linear system with real parameters are also investigated.Examples of methods up to the order p=4 and stage order q—p are provided.Numerical examples on six partitioned test systems confirm that the derived methods achieve the expected order of convergence for large range of stepsizes of integration,and they are also suitable for preserving the accuracy in the stiff limit or preserving the positivity of the numerical solution for large stepsizes.
基金supported by the Natural Science Foundation of China under Grant No.61202154 and No.61133009the National Basic Research Project of China under Grant No.2011CB302203+2 种基金Shanghai Pujiang Program under Grant No.13PJ1404500the Science and Technology Commission of Shanghai Municipality Program under Grant No.13511505000the Open Project Program of the State Key Lab of CAD&CG of Zhejiang University under Grant No.A1401
文摘Regularized Boolean operations have been widely used in 3D modeling systems. However, evaluating Boolean operations may be quite numerically unstable and time consuming, especially for iterated set operations. A novel and unified technique is proposed in this paper for computing single and iterated set operations efficiently, robustly and exactly. An adaptive octree is combined with a nested constructive solid geometry （CSG） tree by this technique. The intersection handling is restricted to the cells in the octree where intersection actually occurs. Within those cells, a CSG tree template is instanced by the surfaces and the tree is converted to planebased binary space partitioning （BSP） for set evaluation; Moreover, the surface classification is restricted to the ceils in the octree where the surfaces only come from a model and are within the bounding-boxes of other polyhedrons. These two ways bring about the efficiency and scalability of the operations, in terms of runtime and memory. As all surfaces in such a cell have the same classification relation, they are classified as a whole. Robustness and exactness are achieved by integrating plane-based geometry representation with adaptive geometry predicate technique in intersection handling, and by applying divide-and-conquer arithmetic on surface classification. Experimental results demonstrate that the proposed approach can guarantee the robustness of Boolean computations and runs faster than other existing approaches.
