examples_in_progress/hamming_sequence.mlw

   1 (*
   2
   3 Hamming sequence is the infinite sequence of integers
   4 1,2,3,4,5,6,8,9,10,12,... divisible by no primes other than 2,3 and 5.
   5
   6 This program computes the n first numbers in this sequence
   7
   8 See Gries, The Science of Programming, page 243
   9
  10 *)
  11
  12
  13 module HammingSequence
  14
  15   use int.Int
  16   use int.MinMax
  17   use number.Divisibility
  18   use number.Prime
  19   use number.Coprime  (* for Euclid's lemma *)
  20
  21   predicate is_hamming (n:int) =
  22     forall d:int. prime d /\ divides d n -> d = 2 \/ d = 3 \/ d = 5
  23
  24   lemma is_hamming_times2 :
  25     forall n:int. n >= 1 -> is_hamming n -> is_hamming (2*n)
  26
  27   lemma is_hamming_times3 :
  28     forall n:int. n >= 1 -> is_hamming n -> is_hamming (3*n)
  29
  30   lemma is_hamming_times5 :
  31     forall n:int. n >= 1 -> is_hamming n -> is_hamming (5*n)
  32
  33   use array.Array
  34   use ref.Ref
  35
  36   let hamming (n:int) : array int
  37     requires { n >= 1 }
  38     ensures  { forall k:int. 0 <= k < n -> is_hamming result[k] }
  39     ensures  { forall k:int. 0 < k < n -> result[k-1] < result[k] }
  40     ensures  { forall k m:int. 0 < k < n ->
  41       result[k-1] < m < result[k] -> not (is_hamming m) }
  42   = let t = make n 0 in
  43     t[0] <- 1;
  44     let x2 = ref 2 in let j2 = ref 0 in
  45     let x3 = ref 3 in let j3 = ref 0 in
  46     let x5 = ref 5 in let j5 = ref 0 in
  47     for i=1 to n-1 do
  48       invariant { forall k:int. 0 <= k < i -> t[k] > 0 }
  49       invariant { forall k:int. 0 < k < i -> t[k-1] < t[k] }
  50       invariant { forall k:int. 0 <= k < i -> is_hamming t[k] }
  51       invariant { 0 <= !j2 < i }
  52       invariant { 0 <= !j3 < i }
  53       invariant { 0 <= !j5 < i }
  54       invariant { !x2 = 2*t[!j2] }
  55       invariant { !x3 = 3*t[!j3] }
  56       invariant { !x5 = 5*t[!j5] }
  57       invariant { !x2 > t[i-1] }
  58       invariant { !x3 > t[i-1] }
  59       invariant { !x5 > t[i-1] }
  60       let next = min !x2 (min !x3 !x5) in
  61       t[i] <- next;
  62       while !x2 <= next do
  63         invariant { 0 <= !j2 <= i }
  64         invariant { !x2 = 2*t[!j2] }
  65         variant { next - !x2 }
  66         assert { !j2 < i };
  67         j2 := !j2+1; x2 := 2*t[!j2]
  68       done;
  69       while !x3 <= next do
  70         invariant { 0 <= !j3 <= i }
  71         invariant { !x3 = 3*t[!j3] }
  72         variant { next - !x3 }
  73         assert { !j3 < i };
  74         j3 := !j3+1; x3 := 3*t[!j3]
  75       done;
  76       while !x5 <= next do
  77         invariant { 0 <= !j5 <= i }
  78         invariant { !x5 = 5*t[!j5] }
  79         variant { next - !x5 }
  80         assert { !j5 < i };
  81         j5 := !j5+1; x5 := 5*t[!j5]
  82       done
  83     done;
  84     t
  85
  86   let test () = hamming 30
  87
  88 end