Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Misleading pretty printing #1

Open
phschmitt27 opened this issue Nov 4, 2018 · 0 comments
Open

Misleading pretty printing #1

phschmitt27 opened this issue Nov 4, 2018 · 0 comments

Comments

@phschmitt27
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant