Analysis of infinite loops using S-formulas

This paper considers formulas of the firstorder predicate logic defined on the abstract state space (briefly S-formulas) that describe three possible behavioral patterns for the WHILE loop: it does not terminate, it potentially terminates and its termination is guaranteed. Based on that, we will analyze the infinite loop and show that its semantics is equivalent to the abort statement. Our approach is solely based on the first order predicate logic, so the analysis may be automated using automatic theorem provers.