The Problem Of Formal Verification Of Generic Program

As the current computer software systems become more and more complex, its development is also increasing difficulty. Traditional development methods mainly rely on manual methods, inefficient, poor quality, accuracy is not guaranteed. Generic programming (Generic Programming, GP) has become another important technology of modern programming. The aim is to represent a class of software is interoperable, generic representation of a broader scope, specific software program by generic instantiation parameter obtained without reducing the operating efficiency.First, This paper describes the generic programming and STL status and development, but also describes the basic components of STL, and discuss the role of generic programming as well as shortcomings in the programming process, there is a brief introduction of generic++STL, C++ template programming relationship with C, described in detail and the importance of using formal methods to verify the correctness of the research program of formal methods.Second, According to the theory of formal semantics and inference rules related chose two specific examples of the STL algorithms that change the sequence of elements in the content exchange, function general numerical calcu algorithm lation numerical calculation algorithm performed to verify and prove the correctness of programs. By axiomatic semantics approach, detailed reasoning verification, this paper gives specific reasoning process validation and verification of the correctness of the results obtained program. Making calculus more general program, making it possible to achieve substantial progress in a number of new formal methods.Again, the subject is also studied and summed up in four generic programming techniques: partial template specialization, often mapped to an integer type, typed on an assembly-type mapping, and other generalized functor. Among them, partial template specialization can specialize template, not for a specific, fixed set of parameters, but for "a consistent pattern of a group of parameters"; often do not allow integer mapped to type at compile numerical (especially boolean) depends on factors as assigned; typed for other mapping type is the use of function overloading to replace the lack of a characteristic C++:function template partial specialization; Detection convertible and inheritance during compilation is to determine whether any two typed It can be converted to each other, or whether the same type, or whether there is inheritance. And this program code four technologies are analyzed and studied to realize the interface to another switch from one interface, and the conversion results are reliable, make the program has improved in erms of reusability.