KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Sat Mar 01 14:33:17 UTC 2025

Overview

infFlow.key

Predicates

newObjectsIsomorphic

newObjectsIsomorphic (Seq , Heap , Seq , Heap ); defined in: infFlow.key Line: 11 Offset :4

newOnHeap

newOnHeap (Heap , Seq ); defined in: infFlow.key Line: 12 Offset :4

sameTypes

sameTypes (Seq , Seq ); defined in: infFlow.key Line: 13 Offset :4

sameType

sameType (any , any ); defined in: infFlow.key Line: 14 Offset :4

objectsIsomorphic

objectsIsomorphic (Seq , Seq , Seq , Seq ); defined in: infFlow.key Line: 15 Offset :4

objectIsomorphic

objectIsomorphic (Seq , Object , Seq , Object ); defined in: infFlow.key Line: 16 Offset :4

Functions

Taclets

No choice condition specified

definitionOfNewObjectsIsomorphic

definitionOfNewObjectsIsomorphic { \schemaVar \term Seq s1 , s2 ; \schemaVar \term Heap h1 , h2 ; \find ( ==> newObjectsIsomorphic ( s1 , h1 , s2 , h2 )) "New on Heap 1" : \replacewith ( ==> newOnHeap ( h1 , s1 )); "New on Heap 2" : \replacewith ( ==> newOnHeap ( h2 , s2 )); "Same Types" : \replacewith ( ==> sameTypes ( s1 , s2 )); "Objects Isomorphic" : \replacewith ( ==> objectsIsomorphic ( s1 , s1 , s2 , s2 )) \heuristics (simplify_enlarging ) };defined in: infFlow.key Line: 24 Offset :4

definitionOfNewOnHeap

definitionOfNewOnHeap { \schemaVar \term Seq s ; \schemaVar \term Heap h ; \schemaVar \variables int i ; \find ( ==> newOnHeap ( h , s )) \varcond \replacewith ( ==> \forall i ; ( ( 0 <= i & i < seqLen ( s ))-> ( ( java.lang.Object :: instance ( any :: seqGet ( s , i ))= TRUE -> boolean :: select ( h , java.lang.Object :: seqGet ( s , i ), java.lang.Object :: )= FALSE )& ( Seq :: instance ( any :: seqGet ( s , i ))= TRUE -> newOnHeap ( h , Seq :: seqGet ( s , i )))))) \heuristics (comprehensions ) };defined in: infFlow.key Line: 42 Offset :4

definitionOfSameTypes

definitionOfSameTypes { \schemaVar \term Seq s1 , s2 ; \schemaVar \variables int i ; \find ( ==> sameTypes ( s1 , s2 )) \varcond \replacewith ( ==> seqLen ( s1 )= seqLen ( s2 )& \forall i ; ( ( 0 <= i & i < seqLen ( s1 ))-> ( ( sameType ( any :: seqGet ( s1 , i ), any :: seqGet ( s2 , i )))& ( Seq :: instance ( any :: seqGet ( s1 , i ))= TRUE -> sameTypes ( Seq :: seqGet ( s1 , i ), Seq :: seqGet ( s2 , i )))))) \heuristics (comprehensions ) };defined in: infFlow.key Line: 61 Offset :4

definitionOfObjectsIsomorphic

definitionOfObjectsIsomorphic { \schemaVar \term Seq s1 , t1 , s2 , t2 ; \schemaVar \variables int i ; \find ( ==> objectsIsomorphic ( s1 , t1 , s2 , t2 )) \varcond \replacewith ( ==> \forall i ; ( ( 0 <= i & i < seqLen ( t1 ))-> ( ( java.lang.Object :: instance ( any :: seqGet ( t1 , i ))= TRUE -> objectIsomorphic ( s1 , java.lang.Object :: seqGet ( t1 , i ), s2 , java.lang.Object :: seqGet ( t2 , i )))& ( Seq :: instance ( any :: seqGet ( t1 , i ))= TRUE -> objectsIsomorphic ( s1 , Seq :: seqGet ( t1 , i ), s2 , Seq :: seqGet ( t2 , i )))))) \heuristics (comprehensions ) };defined in: infFlow.key Line: 79 Offset :4

definitionOfObjectIsomorphic

definitionOfObjectIsomorphic { \schemaVar \term Seq s1 , s2 ; \schemaVar \term Object o1 , o2 ; \schemaVar \variables int i ; \find ( ==> objectIsomorphic ( s1 , o1 , s2 , o2 )) \varcond \replacewith ( ==> \forall i ; ( ( 0 <= i & i < seqLen ( s1 ))-> ( ( java.lang.Object :: instance ( any :: seqGet ( s1 , i ))= TRUE -> ( java.lang.Object :: seqGet ( s1 , i )= o1 <-> java.lang.Object :: seqGet ( s2 , i )= o2 ))& ( Seq :: instance ( any :: seqGet ( s1 , i ))= TRUE -> objectIsomorphic ( Seq :: seqGet ( s1 , i ), o1 , Seq :: seqGet ( s2 , i ), o2 ))))) \heuristics (comprehensions ) };defined in: infFlow.key Line: 107 Offset :4

sameTypeTrue

sameTypeTrue { \schemaVar \term any x1 , x2 ; \assumes ( G :: exactInstance ( x1 )= TRUE , G :: exactInstance ( x2 )= TRUE ==> ) \find ( sameType ( x1 , x2 )) \replacewith ( true ) \heuristics (concrete ) };defined in: infFlow.key Line: 134 Offset :4

sameTypeFalse

sameTypeFalse { \schemaVar \term any x1 , x2 ; \assumes ( G :: exactInstance ( x1 )= TRUE , H :: exactInstance ( x2 )= TRUE ==> ) \find ( sameType ( x1 , x2 )) \varcond \replacewith ( false ) \heuristics (concrete ) };defined in: infFlow.key Line: 145 Offset :4