hoey@ai.etl.army.mil (Dan Hoey) (08/18/90)
In article <24279@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes: >... It's really quite trivial to prove that recursion is >impossible in most non-recursive programs. The only programs where >non-recursion cannot be proven automatically are those which have a >recursive call in a section of code that will never be executed, but >where the compiler cannot prove that the code will never be executed. >Since such programs are almost guaranteed to be not what the >programmer intended, I feel confident in saying that non-recursion can >be automatically proven in correct non-recursive programs. That's true of simple recursion, but mutually recursive program units (functions or subroutines) are more problematical. It is permissible in (nonrecursive) Fortran to have unit A contain a call to unit B and vice versa as long as A never calls B when A was called by B (and v.v.). Such ``lexically recursive'' units are useful, and their failure to perform the forbidden dynamically recursive calls cannot be verified before run time. Dan
gudeman@cs.arizona.edu (David Gudeman) (08/18/90)
In article <90@ai.etl.army.mil> hoey@ai.etl.army.mil (Dan Hoey) writes: >In article <24279@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) sticks his foot in his mouth: > >>... I feel confident in saying that non-recursion can >>be automatically proven in correct non-recursive programs. > >That's true of simple recursion, but mutually recursive program units >(functions or subroutines) are more problematical... Grumble. I also forgot the problems with procedures-valued variables (we were talking about C weren't we?). Oh well, you can still detect a _large_ majority of non-recursive programs... -- David Gudeman Department of Computer Science The University of Arizona gudeman@cs.arizona.edu Tucson, AZ 85721 noao!arizona!gudeman