摘要：Generic programming has emerged as a paradigm for the development of highly reusable and safe software libraries. Generic constraint mechanism can detect and verify the validity of generic parameter instantiated, thereby guarantee dependability and safety of generic programming. Kleene algorithm is ingenious for solving general network path problems but there is a lack of research concerning how to verify the closed semi-ring constraint of the algorithm. First, the paper describes the related works of generic constraints. Next, based on a new description of generic constraints of Apla language by means of algebraic structures, presents the case of generic Kleene algorithm, which is hard to describe and verify its constraint by the current method. Then, with the help of Isabelle theorem prover, verifies closed semi-ring constraint of Kleene algorithm. Finally, transforms the Apla programs of generic Kleene algorithm to C++ codes automatically based on C++ generator. Success in this example gives us more evidence that the approach does not only support for appropriate semantic constraints, but also markedly improves dependability and safety of generic programming.
