KeY Logic Documentation

Defined symbols in the KeY System

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

Overview

loopInvariantRules.key

Sorts

Taclets

No choice condition specified

crossInst

crossInst { \assumes ( ==> ( ( k <= - 1 | k >= i )| c )) \find ( \forall v ; ( ( ( v <= - 1 | v >= j )| b )| a )==> ) \varcond \add ( sk = k & {\subst v ; sk } ( ( ( v <= - 1 | v >= j )| b )| a )==> ) \heuristics (loopInvariant ) };defined in: loopInvariantRules.key Line: 19 Offset :4

cutUpperBound

cutUpperBound { \assumes ( \forall v ; ( ( ( v <= - 1 | v >= j )| b )| a )==> ) \find ( ==> ( ( k <= - 1 | k >= i )| c )) \add ( ( k = i )==> ); \add ( ( k != i )==> ) \heuristics (loopInvariant ) };defined in: loopInvariantRules.key Line: 27 Offset :4