Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / integer_division.org @ 8cc55e2c

History | View | Annotate | Download (1.32 KB)

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 mod_C b < 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 mod_C b < 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 mod_C < 0 ? abs(b) : 0)
39
          = a mod_M b - ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0)
40
            (using the def of mod_M above)
41

    
42
a div_C b = (a - (a mod_C b)) div_M b
43
          
44
Let's choose the second, simpler, def of mod_C
45