Title :
Analysis of infinite loops using S-formulas
Author :
Malbaski, D. ; Kupusinac, A.
Author_Institution :
Fac. of Tech. Sci., Univ. of Novi Sad, Novi Sad, Serbia
Abstract :
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.
Keywords :
formal logic; program control structures; program verification; programming language semantics; theorem proving; S-formulas; WHILE loop; abstract state space; automatic theorem provers; behavioral patterns; first-order predicate logic; infinite loop analysis; loop semantics; programming languages; Abstracts; Computers; Programming profession; Semantics; Syntactics; Vectors; loop semantics; theory of programming;
Conference_Titel :
Telecommunications Forum (TELFOR), 2012 20th
Conference_Location :
Belgrade
Print_ISBN :
978-1-4673-2983-5
DOI :
10.1109/TELFOR.2012.6419522