The KeY systems pretty prints div(a,b) as a/b and mod(a,b) as a%b. This is misleading since
div(a,b) and a/b have different semantics. As a consequence also the semantics of mod(a,b)
and a%b disagree. More precisely the semantics of div(a,b) is the Euclidean semantics while
a/b enjoys the Java semantics (truncating towards 0) ignoring overflow.
Surprisingly, pretty printing does not change jdiv and jmod. Though they share the same
semantics as a/b and a%b.
I would prefer pretty printing should not change the rendering of div and mod.
The KeY systems pretty prints div(a,b) as a/b and mod(a,b) as a%b. This is misleading since
div(a,b) and a/b have different semantics. As a consequence also the semantics of mod(a,b)
and a%b disagree. More precisely the semantics of div(a,b) is the Euclidean semantics while
a/b enjoys the Java semantics (truncating towards 0) ignoring overflow.
Surprisingly, pretty printing does not change jdiv and jmod. Though they share the same
semantics as a/b and a%b.
I would prefer pretty printing should not change the rendering of div and mod.