Email Gateway (Aug 19 2022 at 13:51): Email Gateway (Aug 19 2022 at 13:51):From: "Jens-D. Doll" <jd@cococo.de>
Hello Rene and Isabelle developers,
having read your loop problems (vs. termination problems) for a while now
I would like to suggest an important improvement to your code, which might
remove infinite loops at once and forever.
When working for the industry in Hamburg in the 80s I was a programmer and
had to make sure that certain functions terminate definitely, which could
not be guaranteed by the recursive code. So I build a second stack in
parallel to the call stack, which was handled at each function entry. The
stack contained the names of the functions called and the simple check
consists of finding the just called function in the stack levels below the
current one. If found, there was a loop in the call sequence and gave a
hint that this might be an infinite one. The practical task was now to
identify a function
loopcheck(functionstack),
which predicted an infinite loop with a high probability. A first approach
should not be that difficult and later improvement of this method should
lead to non looping Isabelle code ...
Have a good Sunday,
Jens
Last updated: Apr 27 2024 at 04:17 UTC