## Revision a6e85cdc

View differences:

doc/integer_division.org
1
Integer division in LustreC

2

3
* Issue

4

5
Integer division / and associated modulo mod

6

7
a = (a / b) * b + (a mod b)

8

9
Division between two integers can be interpreted in different ways

10
- a C like division where sign(a mod b) = sign a

11
- a euclidean division where 0 <= a mod b < |b|

12
In both cases they satisfy the above equation.

13

14
Kind model-checker or Horn encoding assumes the mathematical definition, ie. the

15
euclidean division, while lustreC or the Verimag compiler rely on the C

16
definition.

17

18
In the following we deonote by div_C/mod_C and div_M/mod_M the functions in C

19
and math, respectively.

20

21
As an example -4 div_C 3 = -1 while -4 div_M 3 = 2

22

23
Some properties:

24
- we have a div_M b = a div_C b when a = b * k

25
- we have a mod_C b = 0 \equiv a mod_M b = 0.

26

27
* From C to Euclidian

28

29
a mod_M b = (a mod_C b) + (a < 0 ? abs(b) : 0)

30

31
a div_M b = (a - (a mod_M b)) div_C b

32
          = (a - ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b

33

34
* From Euclidian to C

35

36
a mod_C b = (a >= 0 ? a mod_M b : - ((-a) mod_M b))

37
            (using math def to ensure positiveness of remainder))

38
          = (a mod_M b) - (a < 0 ? abs(b) : 0)

39
            (using the def of mod_M above)

40

41
a div_C b = (a - (a mod_C b)) div_M b

42
          = (a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b

43


44
Let's chosse the second, simpler, def of mod_C

45

Also available in: Unified diff