examples/division.mlw

   1
   2 (** Euclidean division *)
   3
   4 module Division
   5
   6   use int.Int
   7   use ref.Refint
   8
   9   let division (a b: int) : int
  10     requires { 0 <= a && 0 < b }
  11     ensures  { exists r. result * b + r = a && 0 <= r < b }
  12   =
  13     let ref q = 0 in
  14     let ref r = a in
  15     while r >= b do
  16       invariant { q * b + r = a && 0 <= r }
  17       variant   { r }
  18       incr q;
  19       r -= b
  20     done;
  21     q
  22
  23 end
  24
  25 (** Euclidean division from Hoare's seminal paper
  26     "An Axiomatic Basis for Computer Programming"
  27     (Communications of the ACM 12(10), 1969).
  28
  29     Hoare's proof of Euclidean division is performed under the nine
  30     axioms for arithmetic given below, which are all valid for several
  31     models of machine arithmetic (infinite arithmetic, strict
  32     interpretation, firm boundary, modulo arithmetic).
  33
  34     Notes:
  35     - Axioms A2 and A4 (commutativity and associativity of multiplication)
  36       are actually not needed for the proof.
  37     - Hoare is not proving termination.
  38 *)
  39
  40 module Hoare
  41
  42   type integer
  43
  44   val constant zero: integer
  45   val constant one: integer
  46   val function (+) (x y: integer) : integer
  47   val function (-) (x y: integer) : integer
  48   val function (*) (x y: integer) : integer
  49   val predicate (<=) (x y: integer)
  50
  51   axiom A1: forall x y. x + y = y + x
  52   axiom A2: forall x y. x * y = y * x
  53   axiom A3: forall x y z. (x + y) + z = x + (y + z)
  54   axiom A4: forall x y z. (x * y) * z = x * (y * z)
  55   axiom A5: forall x y z. x * (y + z) = x * y + x * z
  56   axiom A6: forall x y. y <= x -> (x - y) + y = x
  57   axiom A7: forall x. x + zero = x
  58   axiom A8: forall x. x * zero = zero
  59   axiom A9: forall x. x * one = x
  60
  61   let division (x y: integer) : (q: integer, r: integer)
  62     ensures  { not (y <= r) }
  63     ensures  { x = r + y * q }
  64     diverges
  65   =
  66     let ref r = x in
  67     let ref q = zero in
  68     while y <= r do
  69       invariant { x = r + y * q }
  70       r <- r - y;
  71       q <- one + q
  72     done;
  73     q, r
  74
  75 end
  76
  77 module HoareSound
  78   use int.Int
  79   clone Hoare with type integer = int, val zero = zero,
  80     val one = one, val (+) = (+), val (-) = (-), val (*) = (*),
  81     val (<=) = (<=), lemma .
  82 end