accDefinition {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term deltaObject o2 ;
\schemaVar \variables Field fv ;
\find ( acc ( h , s , o , o2 ))
\varcond \replacewith ( o != null & o2 != null & \exists fv ; ( elementOf ( o , fv , s )& deltaObject :: select ( h , o , fv )= o2 ))
\heuristics (simplify )
};defined in: reachRules.key Line: 11 Offset :4reachDefinition {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , n ))
\varcond \replacewith ( n >= 0 & o != null & o2 != null & ( n = 0 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n - 1 )& acc ( h , s , ov , o2 ))))
};defined in: reachRules.key Line: 30 Offset :4reachZero {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\find ( reach ( h , s , o , o2 , 0 ))
\replacewith ( o != null & o = o2 )
\heuristics (simplify )
};defined in: reachRules.key Line: 57 Offset :4reachOne {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\find ( reach ( h , s , o , o2 , 1 ))
\replacewith ( acc ( h , s , o , o2 ))
\heuristics (simplify )
};defined in: reachRules.key Line: 69 Offset :4reachNull {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term int n ;
\find ( reach ( h , s , o , null , n ))
\replacewith ( false )
\heuristics (simplify )
};defined in: reachRules.key Line: 81 Offset :4reachNull2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o2 ;
\schemaVar \term int n ;
\find ( reach ( h , s , null , o2 , n ))
\replacewith ( false )
\heuristics (simplify )
};defined in: reachRules.key Line: 94 Offset :4reachAddOne {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , 1 + n ))
\varcond \replacewith ( n >= - 1 & o != null & o2 != null & ( n = - 1 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n )& acc ( h , s , ov , o2 ))))
\heuristics (simplify )
};defined in: reachRules.key Line: 107 Offset :4reachAddOne2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , n + 1 ))
\varcond \replacewith ( n >= - 1 & o != null & o2 != null & ( n = - 1 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n )& acc ( h , s , ov , o2 ))))
\heuristics (simplify )
};defined in: reachRules.key Line: 131 Offset :4reachUniquePathSameSteps {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ), o , o2 , n )==> )
\find ( reach ( h , allObjects ( f ), o , o3 , n )==> )
\varcond \add ( o2 = o3 ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 155 Offset :4reachEndOfUniquePath {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n , n2 ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ), o , o2 , n ), alpha :: select ( h , o2 , f )= null , alpha :: select ( h , o3 , f )= null ==> )
\find ( reach ( h , allObjects ( f ), o , o3 , n2 )==> )
\varcond \add ( o2 = o3 & n = n2 ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 171 Offset :4reachEndOfUniquePath2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n , n2 ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ), o , o2 , n ), alpha :: select ( h , o2 , f )= null ==> )
\find ( reach ( h , allObjects ( f ), o , o3 , n2 )==> )
\varcond \add ( n2 < n | ( o2 = o3 & n = n2 )==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 189 Offset :4reachDependenciesStoreSimple {
\schemaVar \term Heap h ;
\schemaVar \term Field f , f2 ;
\schemaVar \term any x ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\find ( reach ( store ( h , o3 , f2 , x ), allObjects ( f ), o , o2 , n ))
\varcond \replacewith ( reach ( h , allObjects ( f ), o , o2 , n ))
\heuristics (simplify )
};defined in: reachRules.key Line: 206 Offset :4reachDependenciesStoreSimpleEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term any x ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\assumes ( store ( h , o3 , f2 , x )= h2 ==> )
\find ( reach ( h2 , allObjects ( f ), o , o2 , n ))
\varcond \replacewith ( reach ( h , allObjects ( f ), o , o2 , n ))
\heuristics (simplify )
};defined in: reachRules.key Line: 221 Offset :4reachDoesNotDependOnCreatedness {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\find ( reach ( create ( h , o3 ), s , o , o2 , n ))
\replacewith ( reach ( h , s , o , o2 , n ))
\heuristics (simplify )
};defined in: reachRules.key Line: 237 Offset :4reachDependenciesStore {
\schemaVar \term Heap h ;
\schemaVar \term Field f ;
\schemaVar \term any x ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \variables int nv ;
\find ( reach ( store ( h , o3 , f , x ), s , o , o2 , n ))
\sameUpdateLevel
\varcond "Dependencies changed" : \add ( ==> ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ))& elementOf ( o3 , f , s )));
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n )) \add ( ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ))& elementOf ( o3 , f , s ))==> )
};defined in: reachRules.key Line: 249 Offset :4reachDependenciesStoreEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term Field f ;
\schemaVar \term any x ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \variables int nv ;
\assumes ( store ( h , o3 , f , x )= h2 ==> )
\find ( reach ( h2 , s , o , o2 , n ))
\sameUpdateLevel
\varcond "Dependencies changed" : \add ( ==> ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ))& elementOf ( o3 , f , s )));
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n )) \add ( ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ))& elementOf ( o3 , f , s ))==> )
};defined in: reachRules.key Line: 278 Offset :4reachDependenciesAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\schemaVar \variables int nv ;
\find ( reach ( anon ( h , s2 , h2 ), s , o , o2 , n ))
\sameUpdateLevel
\varcond "Dependencies changed" : \add ( ==> \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 )& \exists nv ; ( nv < n & reach ( h , s , o , ov , nv ))& elementOf ( ov , fv , s )));
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n )) \add ( \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 )& \exists nv ; ( nv < n & reach ( h , s , o , ov , nv ))& elementOf ( ov , fv , s ))==> )
};defined in: reachRules.key Line: 308 Offset :4reachDependenciesAnonCoarse {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\schemaVar \variables int nv ;
\find ( reach ( anon ( h , s2 , h2 ), s , o , o2 , n ))
\sameUpdateLevel
\varcond "Dependencies changed" : \add ( ==> \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 )& \exists nv ; ( reach ( h , s , o , ov , nv ))& elementOf ( ov , fv , s )));
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n )) \add ( \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 )& \exists nv ; ( reach ( h , s , o , ov , nv ))& elementOf ( ov , fv , s ))==> )
};defined in: reachRules.key Line: 350 Offset :4only_created_objects_are_reachable {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\assumes ( wellFormed ( h )==> o = null )
\find ( reach ( h , s , o , o2 , n )==> )
\add ( ! boolean :: select ( h , o , java.lang.Object :: )= TRUE | boolean :: select ( h , o2 , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 392 Offset :4reach_does_not_depend_on_fresh_locs {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\assumes ( ==> o = null )
\find ( reach ( anon ( h , empty , h2 ), s , o , o2 , n ))
\replacewith ( reach ( h , s , o , o2 , n ));
\add ( ==> wellFormed ( h )& boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: reachRules.key Line: 405 Offset :4reach_does_not_depend_on_fresh_locs_EQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , empty , h2 )= EQ ==> o = null )
\find ( reach ( EQ , s , o , o2 , n ))
\replacewith ( reach ( h , s , o , o2 , n ));
\add ( ==> wellFormed ( h )& boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: reachRules.key Line: 420 Offset :4