The SPARK Ada language prevents recursion by only allowing you to call methods that are defined above the method you are in. It has a similar rule to prevent re

The SPARK Ada language prevents recursion by only allowing you to call methods that are defined above the method you are in. It has a similar rule to prevent recursive calls between packages although I forget the details of that. From this you can calculate the worst case stack size. As all other memory has to be statically allocated you can always caclculate the maximum memory footprint of any progam. Obviously those restrictions mean you have to write your code without recursion, but in practice the uses that SPARK is put to don't tend to need it. A statically allocated stack in your code and a loop can solve a lot of problems (along with suitable logic for gracefully handling that stack filling up).