| 摘要 |
A method for ensuring that a program using dynamic binding and recursion is free from unbounded recursion is provided, together with a method for automatically constructing a set of mathematical theorems that are all true theorems if the program is indeed free from unbounded recursion. In a preferred embodiment, a computer program generates the set of theorems automatically from information in the program and the same or another computer program attempts to prove the theorems, with or without human assistance.
|
