janhaag/PSE2011 — Issue #62: description of "/" and "%" wrong
Author: ratefuchs
Created: 2012-02-28 16:59:42+00:00
State: open
Labels: Documentation

"/" does not round to zero. It is more complicated as it uses SMTLib definitions; see
http://goedel.cs.uiowa.edu/smtlib/theories/Ints.smt2
for more details (this also affects "%" definition).

"/" and "%" by zero are not needed as we have the implicit checks before those statements; and we don't recover from Specification failure. However, description of the implicit checks should be given.

The interpreter stops one additional time on each "%", not only on "/".