KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Jun 05 00:10:27 UTC 2026

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 ))-> ( ( instance <[ java.lang.Object ]> ( seqGet <[ any ]> ( s , i ))= TRUE -> select <[ boolean ]> ( h , seqGet <[ java.lang.Object ]> ( s , i ), java.lang.Object :: #$created)= FALSE )& ( instance <[ Seq ]> ( seqGet <[ any ]> ( s , i ))= TRUE -> newOnHeap ( h , seqGet <[ Seq ]> ( 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 ( seqGet <[ any ]> ( s1 , i ), seqGet <[ any ]> ( s2 , i )))& ( instance <[ Seq ]> ( seqGet <[ any ]> ( s1 , i ))= TRUE -> sameTypes ( seqGet <[ Seq ]> ( s1 , i ), seqGet <[ Seq ]> ( 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 ))-> ( ( instance <[ java.lang.Object ]> ( seqGet <[ any ]> ( t1 , i ))= TRUE -> objectIsomorphic ( s1 , seqGet <[ java.lang.Object ]> ( t1 , i ), s2 , seqGet <[ java.lang.Object ]> ( t2 , i )))& ( instance <[ Seq ]> ( seqGet <[ any ]> ( t1 , i ))= TRUE -> objectsIsomorphic ( s1 , seqGet <[ Seq ]> ( t1 , i ), s2 , seqGet <[ Seq ]> ( 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 ))-> ( ( instance <[ java.lang.Object ]> ( seqGet <[ any ]> ( s1 , i ))= TRUE -> ( seqGet <[ java.lang.Object ]> ( s1 , i )= o1 <-> seqGet <[ java.lang.Object ]> ( s2 , i )= o2 ))& ( instance <[ Seq ]> ( seqGet <[ any ]> ( s1 , i ))= TRUE -> objectIsomorphic ( seqGet <[ Seq ]> ( s1 , i ), o1 , seqGet <[ Seq ]> ( s2 , i ), o2 ))))) \heuristics (comprehensions ) };defined in: infFlow.key Line: 107 Offset :4

sameTypeTrue

sameTypeTrue { \schemaVar \term any x1 , x2 ; \assumes ( exactInstance <[ G ]> ( x1 )= TRUE , exactInstance <[ G ]> ( 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 ( exactInstance <[ G ]> ( x1 )= TRUE , exactInstance <[ H ]> ( x2 )= TRUE ==> ) \find ( sameType ( x1 , x2 )) \varcond \replacewith ( false ) \heuristics (concrete ) };defined in: infFlow.key Line: 145 Offset :4