Penalty model for delay of bidding section construction period in South-to-North Water Diversion Eastern Route Project from perspective of programs

According to the multi-project and program management theory, this paper analyzes the program generation principle and establishes a program based on progress goals. On the basis of the present situation of calculation of penalty for delay of the bidding section construction period with the critical path method, we studied the effects of contractor-induced delay of the bidding section construction period in detail, including the effects on the construction period of the bidding section itself, the earliest start times of the next bidding section and other subsequent bidding sections, and the construction period of the program, and then constructed a penalty model for delay of the bidding section construction period from the perspective of programs. Using the penalty model, we conducted a practical analysis of penalty for delay of the construction period of the Baoying station program in the South-to-North Water Diversion Project. The model can help determine the amount of penalty for delay of the construction period in bidding sections scientifically and reasonably,

Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules

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 Method for Sequential Statistics Class Algorithm Based on Bidirectional Scanning Induction

The program construction process is based on rigorous mathematical reasoning,which leads to a fully correct algorithmic program via step-by-step refinement of the program specifications.The existing program construction methods'refinement process is partly based on individual subjective speculation and analysis,which lacks a precise guidance method.Meanwhile,efficiency factors have usually been ignored in the construction process,and most of the constructed abstract programs cannot be run directly by machines.In order to solve these problems,a novel program construction method for the sequence statistical class algorithms based on bidirectional scan induction is proposed in this paper.The method takes into account the efficiency factor and thus improves the Morgan's refinement calculus.Furthermore,this paper validates the method's feasibility using an efficiency-sensitive sequential statistics class algorithm as a program construction example.The method proposed in this paper realizes the correctness construction process from program specifications to efficient executable programs.