KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:48 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