Merge branch 'fix_session_sudoku' into 'master'
[why3.git] / bench / extraction / 852_int16 / 852_int16.mlw
blob7d0b27a80a63f4c7b329c1cb6de9341ed05129b0
2 module Threshold
4 use int.Int
5 use int.EuclideanDivision
6 use mach.int.Int16
9 end
13 module BCD
15 use int.Int
16 use int.EuclideanDivision
17 use mach.int.UInt16
19 function bcd_log (src : int) : int =
20   let dig1 = div src 1000 in
21   let r1 = mod src 1000 in
22   let dig2 = div r1 100 in
23   let r2 = mod r1 100 in
24   let dig3 = div r2 10 in
25   let dig4 = mod r2 10 in
26   dig1*4096 + dig2*256 + dig3*16 + dig4
29 let bcd_compute (src : uint16) : uint16
30   requires {  0 <= src <= 9999 }
31   ensures { uint16'int result = bcd_log (uint16'int src) }
33   let dig1 = src / 1000 in
34   let r1 = src % 1000 in
35   let dig2 = r1 / 100 in
36   let r2 = r1 % 100 in
37   let dig3 = r2 / 10 in
38   let dig4 = r2 % 10 in
39   dig1*4096 + dig2*256 + dig3*16 + dig4
43 end