However, they fail runtime checking! In contrast, the following pass runtime checking but fail verification:
assert (-6) / 4 == -1
assert (-6) % 4 == -2
The latter is what I would expect from a reasonable programming language, whilst the former is nuts.
NOTE: The reason this is happening is almost certainly due to the semantics implemented by Boogie. For example, Dafny exhibits the same behaviour (which it refers to as Euclidean division).
ALSO: The languages java, rust, go and solidity (amongst others) all follow non-Euclidean division (like the runtime semantics of Whiley). Therefore, its pretty clear which is the right semantic!!
Currently, the following passes verification:
However, they fail runtime checking! In contrast, the following pass runtime checking but fail verification:
The latter is what I would expect from a reasonable programming language, whilst the former is nuts.
NOTE: The reason this is happening is almost certainly due to the semantics implemented by Boogie. For example, Dafny exhibits the same behaviour (which it refers to as Euclidean division).
ALSO: The languages
java,rust,goandsolidity(amongst others) all follow non-Euclidean division (like the runtime semantics of Whiley). Therefore, its pretty clear which is the right semantic!!