KeY Logic Documentation
Defined symbols in the KeY System
Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026
Startpage
Usage Index
KeY Docs
Overview
Taclets
wd_Numerical_Cast_Byte
wd_Numerical_Cast_ByteOverFlow
wd_Numerical_Cast_Char
wd_Numerical_Cast_CharOverFlow
wd_Numerical_Cast_Int
wd_Numerical_Cast_IntOverFlow
wd_Numerical_Cast_Long
wd_Numerical_Cast_LongOverFlow
wd_Numerical_Cast_Short
wd_Numerical_Cast_ShortOverFlow
wd_Numerical_Const
wd_Numerical_Const_C
wd_Numerical_Const_Z
wd_Numerical_Mod_Byte
wd_Numerical_Mod_Char
wd_Numerical_Mod_Int
wd_Numerical_Mod_Long
wd_Numerical_Mod_Short
wd_Numerical_Op_Add
wd_Numerical_Op_AddInt
wd_Numerical_Op_AddIntOverFlow
wd_Numerical_Op_AddJInt
wd_Numerical_Op_AddJLong
wd_Numerical_Op_AddLong
wd_Numerical_Op_AddLongOverFlow
wd_Numerical_Op_AndJInt
wd_Numerical_Op_AndJLong
wd_Numerical_Op_BitAndInt
wd_Numerical_Op_BitAndLong
wd_Numerical_Op_BitNegInt
wd_Numerical_Op_BitNegLong
wd_Numerical_Op_BitOrInt
wd_Numerical_Op_BitOrLong
wd_Numerical_Op_BitXOrInt
wd_Numerical_Op_BitXOrLong
wd_Numerical_Op_CheckedAddInt
wd_Numerical_Op_CheckedAddLong
wd_Numerical_Op_CheckedBitNegInt
wd_Numerical_Op_CheckedBitNegLong
wd_Numerical_Op_CheckedBitwiseAndInt
wd_Numerical_Op_CheckedBitwiseOrInt
wd_Numerical_Op_CheckedBitwiseOrLong
wd_Numerical_Op_CheckedBitwiseXOrInt
wd_Numerical_Op_CheckedBitwiseXOrLong
wd_Numerical_Op_CheckedDivInt
wd_Numerical_Op_CheckedDivLong
wd_Numerical_Op_CheckedMinusInt
wd_Numerical_Op_CheckedMinusLong
wd_Numerical_Op_CheckedMulInt
wd_Numerical_Op_CheckedMulLong
wd_Numerical_Op_CheckedShiftLeftInt
wd_Numerical_Op_CheckedShiftLeftLong
wd_Numerical_Op_CheckedShiftRightInt
wd_Numerical_Op_CheckedShiftRightLong
wd_Numerical_Op_CheckedSubInt
wd_Numerical_Op_CheckedSubLong
wd_Numerical_Op_CheckedUShiftRightInt
wd_Numerical_Op_CheckedUShiftRightLong
wd_Numerical_Op_Div
wd_Numerical_Op_DivInt
wd_Numerical_Op_DivIntOverFlow
wd_Numerical_Op_DivJInt
wd_Numerical_Op_DivJLong
wd_Numerical_Op_DivLong
wd_Numerical_Op_DivLongOverFlow
wd_Numerical_Op_JDiv
wd_Numerical_Op_JMod
wd_Numerical_Op_JavaMod
wd_Numerical_Op_JavaModOverFlow
wd_Numerical_Op_JavaShiftLeftInt
wd_Numerical_Op_JavaShiftLeftLong
wd_Numerical_Op_JavaShiftRightInt
wd_Numerical_Op_JavaShiftRightLong
wd_Numerical_Op_JavaUnsignedShiftRightInt
wd_Numerical_Op_JavaUnsignedShiftRightLong
wd_Numerical_Op_MinusInt
wd_Numerical_Op_MinusIntOverFlow
wd_Numerical_Op_MinusJInt
wd_Numerical_Op_MinusJLong
wd_Numerical_Op_MinusLong
wd_Numerical_Op_MinusLongOverFlow
wd_Numerical_Op_Mod
wd_Numerical_Op_ModJInt
wd_Numerical_Op_ModJLong
wd_Numerical_Op_Mul
wd_Numerical_Op_MulInt
wd_Numerical_Op_MulIntOverFlow
wd_Numerical_Op_MulJInt
wd_Numerical_Op_MulJLong
wd_Numerical_Op_MulLong
wd_Numerical_Op_MulLongOverFlow
wd_Numerical_Op_Neg
wd_Numerical_Op_OrJInt
wd_Numerical_Op_OrJLong
wd_Numerical_Op_ShiftLeftInt
wd_Numerical_Op_ShiftLeftLong
wd_Numerical_Op_ShiftRightInt
wd_Numerical_Op_ShiftRightLong
wd_Numerical_Op_Sub
wd_Numerical_Op_SubInt
wd_Numerical_Op_SubIntOverFlow
wd_Numerical_Op_SubJInt
wd_Numerical_Op_SubJLong
wd_Numerical_Op_SubLong
wd_Numerical_Op_SubLongOverFlow
wd_Numerical_Op_UShiftRightInt
wd_Numerical_Op_UShiftRightLong
wd_Numerical_Op_XorJInt
wd_Numerical_Op_XorJLong
wd_Numerical_Op_checkedBitwiseAndLong
wd_Numerical_Pred_Geq
wd_Numerical_Pred_Gt
wd_Numerical_Pred_InByte
wd_Numerical_Pred_InChar
wd_Numerical_Pred_InInt
wd_Numerical_Pred_InLong
wd_Numerical_Pred_InShort
wd_Numerical_Pred_Leq
wd_Numerical_Pred_Lt
wd_Numerical_Pred_WellOrdered
wd_Numerical_Pred_inRangeByte
wd_Numerical_Pred_inRangeChar
wd_Numerical_Pred_inRangeInt
wd_Numerical_Pred_inRangeLong
wd_Numerical_Pred_inRangeShort
wd_Numerical_Quant_Bprod
wd_Numerical_Quant_Bsum
wd_Numerical_Quant_Max
wd_Numerical_Quant_Min
wd_Numerical_Quant_Prod
wd_Numerical_Quant_Sum
wdNumericalRules.key
Taclets
Enabled under choices:
wdChecks:on
wd_Numerical_Const