examples/anagrammi.mlw

   1
   2 (** {1 Anagrammi}
   3
   4   In Umberto Eco's "Foucault's Pendulum" (Il pendolo di Foucault,
   5   1988), there is a short BASIC program that computes the 24
   6   permutations of four letters. It is as follows:
   7   {h<pre>
   8     10 REM anagrammi
   9     20 INPUT L$(1), L$(2), L$(3), L$(4)
  10     30 PRINT
  11     40 FOR I1 = 1 TO 4
  12     50 FOR I2 = 1 TO 4
  13     60 IF I2=I1 THEN 130
  14     70 FOR I3 = 1 TO 4
  15     80 IF I3=I1 THEN 120
  16     90 IF I3=i2 THEN 120
  17    100 LET I4 = 10-(I1+I2+I3)
  18    110 LPRINT L$(I1); L$(I2); L$(I3); L$(I4)
  19    120 NEXT I3
  20    130 NEXT I2
  21    140 NEXT I1
  22    150 END
  23   </pre>}
  24
  25   Note: In the French edition (Grasset, 2013), there is a typo
  26   on line 80, with `=11` instead of `=I1`. And the dollar symbols
  27   are replaced with the letter S.
  28
  29   I could not resist implementing it in WhyML and verifying it,
  30   which is a simple, yet enjoyable, exercise.
  31
  32   Author: Jean-Christophe Filliâtre (CNRS)
  33 *)
  34
  35 use int.Int
  36 use seq.Seq
  37 use seq.Mem
  38 use seq.Distinct
  39
  40 (** A line printed on the output by the program is
  41     a sequence of (4) integers. *)
  42 type line = seq int
  43
  44 (** The line `s` is a permutation of `1234`. *)
  45 predicate perm4 (s: line) =
  46   length s = 4 && (forall i. 0 <= i < 4 -> 1 <= s[i] <= 4) &&
  47   distinct s
  48
  49 (** The program outputs the permutations in lexicographic
  50     order, so we introduce this order relation. *)
  51 predicate lt (s1 s2: line) =
  52   exists i. 0 <= i < 4 && s1[i] < s2[i] &&
  53     forall j. 0 <= j < i -> s1[j] = s2[j]
  54
  55 lemma lt_trans:
  56   forall s1 s2 s3. perm4 s1 -> perm4 s2 -> perm4 s3 ->
  57   lt s1 s2 -> lt s2 s3 -> lt s1 s3
  58
  59 (** A sequence of lines contains only permutations
  60     and is sorted. *)
  61 predicate sorted (o: seq line) =
  62   (* only permutations *)
  63   (forall j. 0 <= j < length o -> perm4 o[j]) &&
  64   (* and they are sorted (and thus all distinct) *)
  65   (forall j1 j2. 0 <= j1 < j2 < length o -> lt o[j1] o[j2])
  66
  67 (** A sequence of lines is sorted and contains exactly
  68     the permutations satisfying predicate `pr`. *)
  69 predicate below (o: seq line) (pr: line -> bool) =
  70   sorted o &&
  71   (forall j. 0 <= j < length o -> pr o[j]) &&
  72   (forall s. perm4 s -> pr s -> mem s o)
  73
  74 (** Shortcut predicates for the loop invariants below: *)
  75 function pr1 (i1: int) : line->bool = fun s ->
  76   s[0]<i1
  77 function pr2 (i1 i2: int) : line->bool = fun s ->
  78   pr1 i1 s || s[0]=i1 && s[1]<i2
  79 function pr3 (i1 i2 i3: int) : line->bool = fun s ->
  80   pr2 i1 i2 s || s[0]=i1 && s[1]=i2 && s[2]<i3
  81
  82 (** The output of the program is modeled with the
  83     following global variable that contains a sequence
  84     of lines. *)
  85 val ref output: seq line
  86
  87 let anagrammi () : unit
  88   requires { output = empty }
  89   ensures  { below output (fun _ -> true) }
  90 = for i1 = 1 to 4 do
  91     invariant { below output (pr1 i1) }
  92     for i2 = 1 to 4 do
  93       invariant { below output (pr2 i1 i2) }
  94       if i2 = i1 then continue;
  95       for i3 = 1 to 4 do
  96         invariant { below output (pr3 i1 i2 i3) }
  97         if i3 = i1 then continue;
  98         if i3 = i2 then continue;
  99         let i4 = 10 - (i1+i2+i3) in
 100         (* LPRINT L$(I1); L$(I2); L$(I3); L$(I4) *)
 101         let line = cons i1 (cons i2 (cons i3 (cons i4 empty))) in
 102         assert { line[0] = i1 && line[1] = i2 &&
 103                  line[2] = i3 && line[3] = i4 };
 104         assert { perm4 line };
 105         output <- snoc output line
 106       done
 107     done
 108   done