bench/extraction/852_int16/852_int16.mlw

   1
   2 module Threshold
   3
   4 use int.Int
   5 use int.EuclideanDivision
   6 use mach.int.Int16
   7
   8
   9 end
  10
  11
  12
  13 module BCD
  14
  15 use int.Int
  16 use int.EuclideanDivision
  17 use mach.int.UInt16
  18
  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
  27
  28
  29 let bcd_compute (src : uint16) : uint16
  30   requires {  0 <= src <= 9999 }
  31   ensures { uint16'int result = bcd_log (uint16'int src) }
  32 =
  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
  40
  41
  42
  43 end