writePermission {
\schemaVar \term Permission p ;
\find ( writePermission ( p ))
\replacewith ( writePermissionObject ( currentThread , p ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 7 Offset :4readPermission {
\schemaVar \term Permission p ;
\find ( readPermission ( p ))
\replacewith ( readPermissionObject ( currentThread , p ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 14 Offset :4permissionDefaultValue {
\find ( Permission :: defaultValue )
\replacewith ( initFullPermission )
\heuristics (simplify )
};defined in: permissionRules.key Line: 21 Offset :4writePermissionObject {
\schemaVar \term Permission p ;
\schemaVar \term Object o ;
\find ( writePermissionObject ( o , p ))
\replacewith ( true )
\heuristics (concrete )
};defined in: permissionRules.key Line: 31 Offset :4readPermissionObject {
\schemaVar \term Permission p ;
\schemaVar \term Object o ;
\find ( readPermissionObject ( o , p ))
\replacewith ( true )
\heuristics (concrete )
};defined in: permissionRules.key Line: 39 Offset :4checkPermissionOwner_empty {
\schemaVar \term Object ow ;
\schemaVar \term int depth ;
\find ( checkPermissionOwner ( ow , depth , emptyPermissionOwnerList ))
"checkPermissionOwner definition" : \replacewith ( false );
"checkPermissionOwner precondition" : \add ( ==> depth >= 0 )
\heuristics (concrete )
};defined in: permissionRules.key Line: 88 Offset :4checkPermissionOwner_nonempty {
\schemaVar \term Object ow , o ;
\schemaVar \term int depth ;
\schemaVar \term PermissionOwnerList ol ;
\find ( checkPermissionOwner ( ow , depth , consPermissionOwnerList ( o , ol )))
"checkPermissionOwner definition" : \replacewith ( \if ( depth = 0 )\then ( ow = o )\else ( checkPermissionOwner ( ow , depth - 1 , ol )));
"checkPermissionOwner precondition" : \add ( ==> depth >= 0 )
\heuristics (simplify_expression )
};defined in: permissionRules.key Line: 100 Offset :4insertPermissionOwner {
\schemaVar \term Object o , no , owner ;
\schemaVar \term int depth ;
\schemaVar \term PermissionOwnerList ol ;
\find ( insertPermissionOwner ( o , no , depth , consPermissionOwnerList ( owner , ol )))
"insertPermissionOwner definition" : \replacewith ( \if ( depth = 0 )\then ( consPermissionOwnerList ( no , consPermissionOwnerList ( owner , ol )))\else ( consPermissionOwnerList ( owner , insertPermissionOwner ( o , no , depth - 1 , ol ))));
"insertPermissionOwner precondition" : \add ( ==> depth >= 0 & checkPermissionOwner ( o , depth , consPermissionOwnerList ( owner , ol )))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 115 Offset :4returnPermissionOwner {
\schemaVar \term Object o , owner ;
\schemaVar \term PermissionOwnerList ol ;
\find ( returnPermissionOwner ( o , consPermissionOwnerList ( owner , ol )))
"returnPermissionOwner definition" : \replacewith ( ol );
"returnPermissionOwner precondition" : \add ( ==> checkPermissionOwner ( o , 0 , consPermissionOwnerList ( owner , ol )))
\heuristics (simplify_expression )
};defined in: permissionRules.key Line: 136 Offset :4transferPermission_empty {
\schemaVar \term boolean split ;
\schemaVar \term Object from , to ;
\schemaVar \term int depth ;
\find ( transferPermission ( split , from , to , depth , emptyPermission ))
\replacewith ( emptyPermission )
\heuristics (concrete )
};defined in: permissionRules.key Line: 150 Offset :4transferPermission_slice {
\schemaVar \term boolean split ;
\schemaVar \term Object from , to ;
\schemaVar \term int depth ;
\schemaVar \term Permission p ;
\schemaVar \term PermissionOwnerList owners ;
\find ( transferPermission ( split , from , to , depth , slice ( owners , p )))
\replacewith ( \if ( from = to )\then ( slice ( owners , p ))\else ( \if ( checkPermissionOwner ( from , depth , owners ))\then ( slice ( insertPermissionOwner ( from , to , depth , owners ), \if ( split = TRUE )\then ( slice ( owners , p ))\else ( transferPermission ( split , from , to , depth , p ))))\else ( slice ( owners , transferPermission ( split , from , to , depth , p )))))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 160 Offset :4returnPermission_empty {
\schemaVar \term Object from , to ;
\find ( returnPermission ( from , to , emptyPermission ))
\replacewith ( emptyPermission )
\heuristics (concrete )
};defined in: permissionRules.key Line: 183 Offset :4returnPermission_slice_split {
\schemaVar \term Object from , to ;
\schemaVar \term Permission p ;
\schemaVar \term PermissionOwnerList owners ;
\find ( returnPermission ( from , to , slice ( consPermissionOwnerList ( from , owners ), slice ( owners , p ))))
"returnPermission definition" : \replacewith ( slice ( owners , returnPermission ( from , to , p )));
"returnPermission precondition" : \add ( ==> from != to & checkPermissionOwner ( to , 0 , owners ))
\heuristics (simplify )
};defined in: permissionRules.key Line: 191 Offset :4returnPermission_slice {
\schemaVar \term Object from , to ;
\schemaVar \term Permission p ;
\schemaVar \term PermissionOwnerList owners ;
\find ( returnPermission ( from , to , slice ( owners , p )))
\replacewith ( \if ( from = to )\then ( slice ( owners , p ))\else ( \if ( checkPermissionOwner ( from , 0 , owners )& checkPermissionOwner ( to , 1 , owners ))\then ( slice ( returnPermissionOwner ( from , owners ), returnPermission ( from , to , p )))\else ( slice ( owners , returnPermission ( from , to , p )))))
\heuristics (simplify_expression )
};defined in: permissionRules.key Line: 204 Offset :4readPermissionSlice {
\schemaVar \term Object o ;
\schemaVar \term PermissionOwnerList ol ;
\schemaVar \term Permission p ;
\find ( readPermissionObject ( o , slice ( ol , p )))
\replacewith ( checkPermissionOwner ( o , 0 , ol )| readPermissionObject ( o , p ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 224 Offset :4readPermissionEmpty {
\schemaVar \term Object o ;
\find ( readPermissionObject ( o , emptyPermission ))
\replacewith ( false )
\heuristics (concrete )
};defined in: permissionRules.key Line: 234 Offset :4writePermissionSlice {
\schemaVar \term Object o ;
\schemaVar \term PermissionOwnerList ol ;
\schemaVar \term Permission p ;
\find ( writePermissionObject ( o , slice ( ol , p )))
\replacewith ( checkPermissionOwner ( o , 0 , ol )& writePermissionObject ( o , p ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 241 Offset :4writePermissionEmpty {
\schemaVar \term Object o ;
\find ( writePermissionObject ( o , emptyPermission ))
\replacewith ( true )
\heuristics (concrete )
};defined in: permissionRules.key Line: 251 Offset :4initFullPermission {
\find ( initFullPermission )
\replacewith ( slice ( consPermissionOwnerList ( currentThread , emptyPermissionOwnerList ), emptyPermission ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 260 Offset :4permOwner1 {
\schemaVar \term Object o1 ;
\find ( owner1 ( o1 ))
\replacewith ( consPermissionOwnerList ( o1 , emptyPermissionOwnerList ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 266 Offset :4permOwner2 {
\schemaVar \term Object o1 , o2 ;
\find ( owner2 ( o1 , o2 ))
\replacewith ( consPermissionOwnerList ( o1 , consPermissionOwnerList ( o2 , emptyPermissionOwnerList )))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 273 Offset :4permOwner3 {
\schemaVar \term Object o1 , o2 , o3 ;
\find ( owner3 ( o1 , o2 , o3 ))
\replacewith ( consPermissionOwnerList ( o1 , consPermissionOwnerList ( o2 , consPermissionOwnerList ( o3 , emptyPermissionOwnerList ))))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 280 Offset :4permOwner4 {
\schemaVar \term Object o1 , o2 , o3 , o4 ;
\find ( owner4 ( o1 , o2 , o3 , o4 ))
\replacewith ( consPermissionOwnerList ( o1 , consPermissionOwnerList ( o2 , consPermissionOwnerList ( o3 , consPermissionOwnerList ( o4 , emptyPermissionOwnerList )))))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 287 Offset :4permSlice1 {
\schemaVar \term PermissionOwnerList pol1 ;
\find ( slice1 ( pol1 ))
\replacewith ( slice ( pol1 , emptyPermission ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 294 Offset :4permSlice2 {
\schemaVar \term PermissionOwnerList pol1 , pol2 ;
\find ( slice2 ( pol1 , pol2 ))
\replacewith ( slice ( pol1 , slice ( pol2 , emptyPermission )))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 301 Offset :4twoPermissions {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\schemaVar \variables PermissionOwnerList ol1 , ol2 ;
\find ( twoPermissions ( o1 , o2 , p ))
\varcond \replacewith ( \exists ol1 , ol2 ; p = slice ( consPermissionOwnerList ( o1 , ol1 ), slice ( consPermissionOwnerList ( o2 , ol2 ), emptyPermission )))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 308 Offset :4nonEmptyPermission {
\schemaVar \term Permission p ;
\schemaVar \variables Permission pp ;
\schemaVar \variables PermissionOwnerList ol ;
\find ( nonEmptyPermission ( p ))
\varcond \replacewith ( \exists ol ; \exists pp ; p = slice ( ol , pp ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 324 Offset :4readPermissionOwe {
\schemaVar \term Permission p ;
\schemaVar \term Object o1 , o2 ;
\schemaVar \variables Permission pp ;
\schemaVar \variables PermissionOwnerList ol ;
\find ( readPermissionOwe ( o1 , o2 , p ))
\varcond \replacewith ( \exists ol ; \exists pp ; p = slice ( consPermissionOwnerList ( o1 , consPermissionOwnerList ( o2 , ol )), pp ))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 334 Offset :4readPermissionOwe2 {
\schemaVar \term Permission p ;
\schemaVar \term Object o1 , o2 ;
\schemaVar \variables Permission pp ;
\schemaVar \variables PermissionOwnerList ol , ol0 ;
\find ( readPermissionOwe2 ( o1 , o2 , p ))
\varcond \replacewith ( \exists ol0 ; \exists ol ; \exists pp ; p = slice ( ol0 , slice ( consPermissionOwnerList ( o1 , consPermissionOwnerList ( o2 , ol )), pp )))
\heuristics (simplify_enlarging )
};defined in: permissionRules.key Line: 351 Offset :4writePermissionImpliesReadPermission {
\schemaVar \term Object o ;
\schemaVar \term Permission p ;
\assumes ( writePermissionObject ( o , p )==> )
\find ( readPermissionObject ( o , p ))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 371 Offset :4readPermissionAfterTransferRead {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\schemaVar \term boolean split ;
\assumes ( readPermissionObject ( o1 , p )==> )
\find ( readPermissionObject ( o2 , transferPermission ( split , o1 , o2 , 0 , p )))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 381 Offset :4readPermissionAfterTransferReadEQ {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p , p1 ;
\schemaVar \term boolean split ;
\assumes ( readPermissionObject ( o1 , p ), transferPermission ( split , o1 , o2 , 0 , p )= p1 ==> )
\find ( readPermissionObject ( o2 , p1 ))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 392 Offset :4readPermissionAfterTransferWrite {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\schemaVar \term boolean split ;
\assumes ( writePermissionObject ( o1 , p )==> )
\find ( readPermissionObject ( o2 , transferPermission ( split , o1 , o2 , 0 , p )))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 403 Offset :4readPermissionAfterTransferWriteEQ {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p , p1 ;
\schemaVar \term boolean split ;
\assumes ( writePermissionObject ( o1 , p ), transferPermission ( split , o1 , o2 , 0 , p )= p1 ==> )
\find ( readPermissionObject ( o2 , p1 ))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 414 Offset :4writePermissionAfterFullTransfer {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\assumes ( writePermissionObject ( o1 , p )==> )
\find ( writePermissionObject ( o2 , transferPermission ( FALSE , o1 , o2 , 0 , p )))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 425 Offset :4writePermissionAfterFullTransferEQ {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p1 , p2 ;
\assumes ( writePermissionObject ( o1 , p2 ), transferPermission ( FALSE , o1 , o2 , 0 , p2 )= p1 ==> )
\find ( writePermissionObject ( o2 , p1 ))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 435 Offset :4writePermissionAfterReturn {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\assumes ( writePermissionObject ( o1 , p )==> )
\find ( writePermissionObject ( o2 , returnPermission ( o1 , o2 , p )))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 445 Offset :4writePermissionAfterReturnEQ {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p1 , p2 ;
\assumes ( writePermissionObject ( o1 , p2 ), returnPermission ( o1 , o2 , p2 )= p1 ==> )
\find ( writePermissionObject ( o2 , p1 ))
\replacewith ( true )
\heuristics (simplify )
};defined in: permissionRules.key Line: 455 Offset :4permissionTransferReturnIdentity {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\find ( returnPermission ( o2 , o1 , transferPermission ( FALSE , o1 , o2 , 0 , p )))
\replacewith ( p )
\heuristics (simplify )
};defined in: permissionRules.key Line: 465 Offset :4permissionTransferReturnIdentityEQ {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p1 , p2 ;
\assumes ( p2 = transferPermission ( FALSE , o1 , o2 , 0 , p1 )==> )
\find ( returnPermission ( o2 , o1 , p2 ))
\replacewith ( p1 )
\heuristics (simplify )
};defined in: permissionRules.key Line: 474 Offset :4writePermissionOtherNoPermissionCurrentRead {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\assumes ( writePermissionObject ( o1 , p )==> o2 = o1 )
\find ( readPermissionObject ( o2 , p ))
\replacewith ( false )
\heuristics (simplify )
};defined in: permissionRules.key Line: 484 Offset :4writePermissionOtherNoPermissionCurrentWrite {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Permission p ;
\assumes ( writePermissionObject ( o1 , p )==> o2 = o1 )
\find ( writePermissionObject ( o2 , p ))
\replacewith ( false )
\heuristics (simplify )
};defined in: permissionRules.key Line: 494 Offset :4createdOnHeapImpliesCreatedOnPermissions {
\schemaVar \term Object o ;
\schemaVar \term Heap h , p ;
\assumes ( wellFormed ( h ), wellFormed ( p ), permissionsFor ( p , h ), boolean :: select ( h , o , java.lang.Object :: )= TRUE ==> )
\find ( boolean :: select ( p , o , java.lang.Object :: ))
\sameUpdateLevel
\replacewith ( TRUE )
\heuristics (simplify )
};defined in: permissionRules.key Line: 506 Offset :4