8 +_signs neg zero pos neg   neg   neg {neg, zero, pos} zero neg zero pos pos {neg, zero, pos} pos pos *_signs neg zero pos <_signs neg zero pos neg pos zero neg neg {t, f} true true zero zero zero zero zero false false true pos neg zero pos pos false false {t, f} Abb. 2: Die abstrakten Operationen +_signs, *_signs, <_signs Der   jeweils   erste   Operand   der   Operationen   steht   in   der   Zeile   und   der   zweite   in   der Spalte     der     Tabelle. Wie    zu    erkennen    ist,    bilden    die    abstrakten    Operationen    das Verhalten    der    konkreten    Operationen    unterschiedlich    genau    ab.    Zum    einen    kann    es Operationen    geben,    deren    Resultate    aus    genau    einem    Wert    bestehen, wie    bei der Operation * _signs. Z um   anderen   kann   es   aber   aufgrund   der Über-Approximation    dazu kommen,   das   der   Wert   des   Resultates   nicht   eindeutig   ist,   sondern   eine   Menge   von Werten   aus   dem   Wertebereich   ist,   wie   bei   den   Operation + signs und  <_signs  zu  sehen  ist. Zum Beispiel bei   der   Addition   zweier   positiver   Zahlen   ist   das   Ergebnis   eindeutig   auch positiv,   währen   die   Addition   einer   negativen   und   einer   positiven   Zahl   kein   eindeutiges Ergebnis   hat.   Hier   kann   das   Resultat   sowohl   positiv,   negativ   als   auch   gleich   Null   sein. Dieses   fehlende   Wissen   über   das   Verhalten   von   abstrakten   Operationen   wird   im   Java Path Finder durch eine nicht-deterministische Auswahl interpretiert. Die   Abstraktion   von   Kontrollstrukturen   eines   Programms   ist   auf   die   Datenabstraktion zurückzuführen.    Dazu sind    die    booleschen    Operationen,    aus    denen    die    Bedingungen von    If-Abfragen    sowie    die    Ein-    bzw.    Ausgangsbedingungen    von    Schleifen    bestehen durch   geeignete   abstrakte   Operationen   zu   ersetzen.   Die   Rümpfe   solcher   Anweisungen sind   dann   als   Blöcke   zu   sehen,   die einmal,   einmal   oder   mehrfach   durchlaufen   werden