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