KeY Logic Documentation

Defined symbols in the KeY System

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

Overview

floatHeader.key

Sorts

fp

fp;defined in: floatHeader.key Line: 7 Offset :4

float

float \extends fp ;defined in: floatHeader.key Line: 8 Offset :4

double

double \extends fp ;defined in: floatHeader.key Line: 9 Offset :4

java.lang.Math

java.lang.Math \extends java.lang.Object ;defined in: floatHeader.key Line: 11 Offset :4

Functions

FP

float FP (numbers ); defined in: floatHeader.key Line: 17 Offset :4

DFP

double DFP (numbers ); defined in: floatHeader.key Line: 18 Offset :4

javaUnaryMinusFloat

float javaUnaryMinusFloat (float ); defined in: floatHeader.key Line: 23 Offset :4

javaAddFloat

float javaAddFloat (float , float ); defined in: floatHeader.key Line: 24 Offset :4

javaSubFloat

float javaSubFloat (float , float ); defined in: floatHeader.key Line: 25 Offset :4

javaMulFloat

float javaMulFloat (float , float ); defined in: floatHeader.key Line: 26 Offset :4

javaDivFloat

float javaDivFloat (float , float ); defined in: floatHeader.key Line: 27 Offset :4

javaModFloat

float javaModFloat (float , float ); defined in: floatHeader.key Line: 28 Offset :4

javaMinFloat

float javaMinFloat (float , float ); defined in: floatHeader.key Line: 29 Offset :4

javaMaxFloat

float javaMaxFloat (float , float ); defined in: floatHeader.key Line: 30 Offset :4

javaAddFloatForbiddenResult

float javaAddFloatForbiddenResult (float , float ); defined in: floatHeader.key Line: 33 Offset :4

javaSubFloatForbiddenResult

float javaSubFloatForbiddenResult (float , float ); defined in: floatHeader.key Line: 34 Offset :4

javaMulFloatForbiddenResult

float javaMulFloatForbiddenResult (float , float ); defined in: floatHeader.key Line: 35 Offset :4

javaDivFloatForbiddenResult

float javaDivFloatForbiddenResult (float , float ); defined in: floatHeader.key Line: 36 Offset :4

addFloat

float addFloat (float , float ); defined in: floatHeader.key Line: 39 Offset :4

subFloat

float subFloat (float , float ); defined in: floatHeader.key Line: 40 Offset :4

mulFloat

float mulFloat (float , float ); defined in: floatHeader.key Line: 41 Offset :4

divFloat

float divFloat (float , float ); defined in: floatHeader.key Line: 42 Offset :4

negFloat

float negFloat (float ); defined in: floatHeader.key Line: 43 Offset :4

absFloat

float absFloat (float ); defined in: floatHeader.key Line: 45 Offset :4

javaUnaryMinusDouble

double javaUnaryMinusDouble (double ); defined in: floatHeader.key Line: 50 Offset :4

javaAddDouble

double javaAddDouble (double , double ); defined in: floatHeader.key Line: 51 Offset :4

javaSubDouble

double javaSubDouble (double , double ); defined in: floatHeader.key Line: 52 Offset :4

javaMulDouble

double javaMulDouble (double , double ); defined in: floatHeader.key Line: 53 Offset :4

javaDivDouble

double javaDivDouble (double , double ); defined in: floatHeader.key Line: 54 Offset :4

javaModDouble

double javaModDouble (double , double ); defined in: floatHeader.key Line: 55 Offset :4

javaMinDouble

double javaMinDouble (double , double ); defined in: floatHeader.key Line: 56 Offset :4

javaMaxDouble

double javaMaxDouble (double , double ); defined in: floatHeader.key Line: 57 Offset :4

javaAddDoubleForbiddenResult

double javaAddDoubleForbiddenResult (double , double ); defined in: floatHeader.key Line: 60 Offset :4

javaSubDoubleForbiddenResult

double javaSubDoubleForbiddenResult (double , double ); defined in: floatHeader.key Line: 61 Offset :4

javaMulDoubleForbiddenResult

double javaMulDoubleForbiddenResult (double , double ); defined in: floatHeader.key Line: 62 Offset :4

javaDivDoubleForbiddenResult

double javaDivDoubleForbiddenResult (double , double ); defined in: floatHeader.key Line: 63 Offset :4

addDouble

double addDouble (double , double ); defined in: floatHeader.key Line: 66 Offset :4

subDouble

double subDouble (double , double ); defined in: floatHeader.key Line: 67 Offset :4

mulDouble

double mulDouble (double , double ); defined in: floatHeader.key Line: 68 Offset :4

divDouble

double divDouble (double , double ); defined in: floatHeader.key Line: 69 Offset :4

negDouble

double negDouble (double ); defined in: floatHeader.key Line: 70 Offset :4

absDouble

double absDouble (double ); defined in: floatHeader.key Line: 72 Offset :4

sinDouble

double sinDouble (double ); defined in: floatHeader.key Line: 75 Offset :4

asinDouble

double asinDouble (double ); defined in: floatHeader.key Line: 76 Offset :4

cosDouble

double cosDouble (double ); defined in: floatHeader.key Line: 77 Offset :4

acosDouble

double acosDouble (double ); defined in: floatHeader.key Line: 78 Offset :4

tanDouble

double tanDouble (double ); defined in: floatHeader.key Line: 79 Offset :4

atan2Double

double atan2Double (double , double ); defined in: floatHeader.key Line: 80 Offset :4

sqrtDouble

double sqrtDouble (double ); defined in: floatHeader.key Line: 81 Offset :4

powDouble

double powDouble (double , double ); defined in: floatHeader.key Line: 82 Offset :4

expDouble

double expDouble (double ); defined in: floatHeader.key Line: 83 Offset :4

atanDouble

double atanDouble (double ); defined in: floatHeader.key Line: 84 Offset :4

Predicates

ltFloat

ltFloat (float , float ); defined in: floatHeader.key Line: 89 Offset :4

gtFloat

gtFloat (float , float ); defined in: floatHeader.key Line: 90 Offset :4

leqFloat

leqFloat (float , float ); defined in: floatHeader.key Line: 91 Offset :4

geqFloat

geqFloat (float , float ); defined in: floatHeader.key Line: 92 Offset :4

eqFloat

eqFloat (float , float ); defined in: floatHeader.key Line: 93 Offset :4

floatIsNaN

floatIsNaN (float ); defined in: floatHeader.key Line: 95 Offset :4

floatIsZero

floatIsZero (float ); defined in: floatHeader.key Line: 96 Offset :4

floatIsNormal

floatIsNormal (float ); defined in: floatHeader.key Line: 97 Offset :4

floatIsSubnormal

floatIsSubnormal (float ); defined in: floatHeader.key Line: 98 Offset :4

floatIsInfinite

floatIsInfinite (float ); defined in: floatHeader.key Line: 99 Offset :4

floatIsPositive

floatIsPositive (float ); defined in: floatHeader.key Line: 100 Offset :4

floatIsNegative

floatIsNegative (float ); defined in: floatHeader.key Line: 101 Offset :4

floatIsNice

floatIsNice (float ); defined in: floatHeader.key Line: 102 Offset :4

ltDouble

ltDouble (double , double ); defined in: floatHeader.key Line: 104 Offset :4

gtDouble

gtDouble (double , double ); defined in: floatHeader.key Line: 105 Offset :4

leqDouble

leqDouble (double , double ); defined in: floatHeader.key Line: 106 Offset :4

geqDouble

geqDouble (double , double ); defined in: floatHeader.key Line: 107 Offset :4

eqDouble

eqDouble (double , double ); defined in: floatHeader.key Line: 108 Offset :4

doubleIsNaN

doubleIsNaN (double ); defined in: floatHeader.key Line: 110 Offset :4

doubleIsZero

doubleIsZero (double ); defined in: floatHeader.key Line: 111 Offset :4

doubleIsNormal

doubleIsNormal (double ); defined in: floatHeader.key Line: 112 Offset :4

doubleIsSubnormal

doubleIsSubnormal (double ); defined in: floatHeader.key Line: 113 Offset :4

doubleIsInfinite

doubleIsInfinite (double ); defined in: floatHeader.key Line: 114 Offset :4

doubleIsPositive

doubleIsPositive (double ); defined in: floatHeader.key Line: 115 Offset :4

doubleIsNegative

doubleIsNegative (double ); defined in: floatHeader.key Line: 116 Offset :4

doubleIsNice

doubleIsNice (double ); defined in: floatHeader.key Line: 117 Offset :4