wdLocSetRules.key

Taclets

Enabled under choices: wdChecks:on

wd_LocSet_AllFields

wd_LocSet_AllFields  {
\find (                    wd   (                    allFields   (                    o ) ) )
\varcond   \replacewith (                     wd   (                    o ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 17 Offset :4

wd_LocSet_AllFieldsArr

wd_LocSet_AllFieldsArr  {
\find (                    wd   (                    allFields   (                    o ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             o !=           null ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 31 Offset :4

wd_LocSet_AllObjects

wd_LocSet_AllObjects  {
\find (                    wd   (                    allObjects   (                    f ) ) )
  \replacewith (                     wd   (                    f ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 45 Offset :4

wd_LocSet_FreshLocs

wd_LocSet_FreshLocs  {
\find (                    wd   (                    freshLocs   (                    h ) ) )
  \replacewith (                     wd   (                    h ) &             wellFormed   (                    h ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 56 Offset :4

wd_LocSet_Singleton

wd_LocSet_Singleton  {
\find (                    wd   (                    singleton   (                    o ,                    f ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    f ) &             o !=           null ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 67 Offset :4

wd_LocSet_Singleton_Static

wd_LocSet_Singleton_Static  {
\find (                    wd   (                    singleton   (                    o ,                    f ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    f ) &             o =           null ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 82 Offset :4

wd_LocSet_Singleton_Arr

wd_LocSet_Singleton_Arr  {
\find (                    wd   (                    singleton   (                    o ,                    arr   (                    i ) ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    i ) &             o !=           null &             leq   (                    0 ,                    i ) &             lt   (                    i ,                    length   (                    o ) ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 97 Offset :4

wd_LocSet_Singleton_Quant

wd_LocSet_Singleton_Quant  {
\find (          \forall    c ;             wd   (                    singleton   (                    o ,                    f ) ) )
\varcond   \replacewith (           \forall    c ;            (                    wd   (                    o ) &             wd   (                    f ) ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 111 Offset :4

wd_LocSet_Union

wd_LocSet_Union  {
\find (                    wd   (                    union   (                    l ,                    s ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 125 Offset :4

wd_LocSet_Intersect

wd_LocSet_Intersect  {
\find (                    wd   (                    intersect   (                    l ,                    s ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 136 Offset :4

wd_LocSet_Diff

wd_LocSet_Diff  {
\find (                    wd   (                    setMinus   (                    l ,                    s ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 146 Offset :4

wd_LocSet_ArrRange

wd_LocSet_ArrRange  {
\find (                    wd   (                    arrayRange   (                    o ,                    i ,                    j ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    i ) &             wd   (                    j ) &             o !=           null &             leq   (                    0 ,                    i ) &             leq   (                    i ,                    j ) &             lt   (                    j ,                    length   (                    o ) ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 157 Offset :4

wd_LocSet_AllElemsArr

wd_LocSet_AllElemsArr  {
\find (                    wd   (                    allElementsOfArray   (                    h ,                    o ,                    l ) ) )
\varcond   \replacewith (                     wd   (                    h ) &             wd   (                    o ) &             wd   (                    l ) &             wellFormed   (                    h ) &             o !=           null &             select  <[ boolean ]>   (                    h ,                    o ,                   java.lang.Object  #$created ) =           TRUE ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 171 Offset :4

wd_LocSet_AllElemsArrLocsets

wd_LocSet_AllElemsArrLocsets  {
\find (                    wd   (                    allElementsOfArrayLocsets   (                    h ,                    o ,                    l ) ) )
\varcond   \replacewith (                     wd   (                    h ) &             wd   (                    o ) &             wd   (                    l ) &             wellFormed   (                    h ) &             o !=           null &             select  <[ boolean ]>   (                    h ,                    o ,                   java.lang.Object  #$created ) =           TRUE ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 186 Offset :4

wd_LocSet_InfiniteUnion

wd_LocSet_InfiniteUnion  {
\find (                    wd   (                    infiniteUnion  {    a ; }  (                    l ) ) )
  \replacewith (           \forall    a ;             wd   (                    l ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 201 Offset :4

wd_LocSet_InfiniteUnion2

wd_LocSet_InfiniteUnion2  {
\find (                    wd   (                    infiniteUnion  {    a ,   b ; }  (                    l ) ) )
  \replacewith (           \forall    a ;            (          \forall    b ;             wd   (                    l ) ) ) 
\heuristics  (simplify )
\displayname   "wd_LocSet_InfiniteUnion" 

};

defined in: wdLocSetRules.key Line: 212 Offset :4

wd_LocSet_Pred_ElementOf

wd_LocSet_Pred_ElementOf  {
\find (                    WD   (                    elementOf   (                    o ,                    f ,                    l ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    f ) &             wd   (                    l ) &             o !=           null ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 224 Offset :4

wd_LocSet_Pred_ElementOf_Static

wd_LocSet_Pred_ElementOf_Static  {
\find (                    WD   (                    elementOf   (                    o ,                    f ,                    l ) ) )
\varcond   \replacewith (                     wd   (                    o ) &             wd   (                    f ) &             wd   (                    l ) &             o =           null ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 238 Offset :4

wd_LocSet_Pred_Subset

wd_LocSet_Pred_Subset  {
\find (                    WD   (                    subset   (                    l ,                    s ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 252 Offset :4

wd_LocSet_Pred_Disjoint

wd_LocSet_Pred_Disjoint  {
\find (                    WD   (                    disjoint   (                    l ,                    s ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 263 Offset :4

wd_LocSet_Pred_InHeap

wd_LocSet_Pred_InHeap  {
\find (                    WD   (                    createdInHeap   (                    l ,                    h ) ) )
  \replacewith (                     wd   (                    l ) &             wd   (                    h ) &             wellFormed   (                    h ) ) 
\heuristics  (simplify )

};

defined in: wdLocSetRules.key Line: 273 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview