KeY Logic Documentation

Defined symbols in the KeY System

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

Overview

javaHeader.key

Sorts

any

any;defined in: javaHeader.key Line: 10 Offset :4

java.lang.Object

java.lang.Object;defined in: javaHeader.key Line: 11 Offset :4

java.lang.Cloneable

\abstract java.lang.Cloneable \extends java.lang.Object ;defined in: javaHeader.key Line: 12 Offset :4

java.io.Serializable

\abstract java.io.Serializable \extends java.lang.Object ;defined in: javaHeader.key Line: 13 Offset :4

alpha

\generic alpha, beta, gamma;defined in: javaHeader.key Line: 15 Offset :4

beta

\generic alpha, beta, gamma;defined in: javaHeader.key Line: 15 Offset :4

gamma

\generic alpha, beta, gamma;defined in: javaHeader.key Line: 15 Offset :4

deltaObject

\generic deltaObject \extends java.lang.Object ;defined in: javaHeader.key Line: 16 Offset :4

G

\generic G;defined in: javaHeader.key Line: 18 Offset :4

H

\generic H;defined in: javaHeader.key Line: 19 Offset :4

J

\generic J \extends G ;defined in: javaHeader.key Line: 20 Offset :4

GOS

\generic GOS \extends Object ;defined in: javaHeader.key Line: 21 Offset :4

alphaObj

\generic alphaObj \extends Object ;defined in: javaHeader.key Line: 22 Offset :4

betaObj

\generic betaObj \extends Object ;defined in: javaHeader.key Line: 23 Offset :4

Functions

alpha::cast

alpha alpha :: cast (any ); defined in: javaHeader.key Line: 28 Offset :4

alpha::exactInstance

boolean alpha :: exactInstance (any ); defined in: javaHeader.key Line: 29 Offset :4

alpha::instance

boolean alpha :: instance (any ); defined in: javaHeader.key Line: 30 Offset :4