KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026

Overview

wdStringRules.key

Taclets

Enabled under choices: wdChecks:on

wd_String_Translate

wd_String_Translate { \find ( wd ( clTranslateInt ( i ) ) ) \replacewith ( wd ( i ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 11 Offset :4

wd_String_RmvZeros

wd_String_RmvZeros { \find ( wd ( clRemoveZeros ( c ) ) ) \replacewith ( wd ( c ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 22 Offset :4

wd_String_Hash

wd_String_Hash { \find ( wd ( clHashCode ( c ) ) ) \replacewith ( wd ( c ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 33 Offset :4

wd_String_IndexOfChar

wd_String_IndexOfChar { \find ( wd ( clIndexOfChar ( c , i , j ) ) ) \replacewith ( wd ( i ) & wd ( j ) & wd ( c ) & leq ( 0 , i ) & leq ( i , j ) & lt ( j , seqLen ( c ) ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 44 Offset :4

wd_String_IndexOfStr

wd_String_IndexOfStr { \find ( wd ( clIndexOfCl ( l , i , c ) ) ) \replacewith ( wd ( c ) & wd ( i ) & wd ( l ) & leq ( 0 , i ) & lt ( add ( i , seqLen ( c ) ) , seqLen ( l ) ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 55 Offset :4

wd_String_LastIndexOfChar

wd_String_LastIndexOfChar { \find ( wd ( clLastIndexOfChar ( c , i , j ) ) ) \replacewith ( wd ( i ) & wd ( j ) & wd ( c ) & leq ( 0 , i ) & leq ( i , j ) & lt ( j , seqLen ( c ) ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 66 Offset :4

wd_String_LastIndexOfStr

wd_String_LastIndexOfStr { \find ( wd ( clLastIndexOfCl ( l , i , c ) ) ) \replacewith ( wd ( c ) & wd ( i ) & wd ( l ) & leq ( 0 , i ) & lt ( add ( i , seqLen ( c ) ) , seqLen ( l ) ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 77 Offset :4

wd_String_Replace

wd_String_Replace { \find ( wd ( clReplace ( c , i , j ) ) ) \replacewith ( wd ( i ) & wd ( j ) & wd ( c ) & leq ( 0 , i ) & leq ( 0 , j ) & lt ( i , seqLen ( c ) ) & lt ( j , seqLen ( c ) ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 88 Offset :4

wd_String_Pred_StartsWith

wd_String_Pred_StartsWith { \find ( WD ( clStartsWith ( l , c ) ) ) \replacewith ( wd ( c ) & wd ( l ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 99 Offset :4

wd_String_Pred_EndsWith

wd_String_Pred_EndsWith { \find ( WD ( clEndsWith ( l , c ) ) ) \replacewith ( wd ( c ) & wd ( l ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 110 Offset :4

wd_String_Pred_Contains

wd_String_Pred_Contains { \find ( WD ( clContains ( l , c ) ) ) \replacewith ( wd ( c ) & wd ( l ) ) \heuristics (simplify ) };defined in: wdStringRules.key Line: 121 Offset :4