## lustrec / doc / integer_division.org @ d4c98bae

History | View | Annotate | Download (1.15 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 mod_M b - ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0) |

37 | |

38 |
a div_C b = (a - (a mod_C b)) div_M b |

39 |
= (a mod_M b <> 0 && a <= 0)?((a - a mod_M b + abs(b)) div_M b) :((a - a mod_M b) div_M b) |