Analysis of Loop Semantics using S-Formulas
Aleksandar Kupusinac, Dušan Malbaški · TEM Journal · 2012
There are three possible behavioral patterns for the WHILE loop: it does not terminate, it potentially terminates and its termination is guaranteed. Based on that, to describe the behavior of the WHILE loop we introduce appropriate formulas of the first-order predicate logic defined on the abstract state space (briefly S-formulas). This paper presents our approach to analyzing the WHILE loop semantics that is solely based on the first order predicate logic.