Semantics of Division and Remainder?

[DavePearce]

Currently, the following passes verification:

  assert (-6) / 4 == -2
  assert (-6) % 4 == 2

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!!