Contact English version

L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à jour sur notre équipe.

Bresenham line drawing algorithm

We prove optimality: for each column x, the point (x,y) which is drawn is the closest to the rational line between (0,0) and (x2,y2).

Bresenham algorithm is interesting because its code only uses linear arithmetic but its proof of optimality requires non-linear arithmetic.

Auteurs: Jean-Christophe Filliâtre

Catégories: Non-linear Arithmetic

Outils: Why3

index 

(* Bresenham line drawing algorithm. *)

module M

  use import int.Int
  use import ref.Ref

  (*  Parameters.
      Without loss of generality, we can take [x1=0] and [y1=0].
      Thus the line to draw joins [(0,0)] to [(x2,y2)]
      and we have [deltax = x2] and [deltay = y2].
      Moreover we assume being in the first octant, i.e.
      [0 <= y2 <= x2]. The seven other cases can be easily
      deduced by symmetry. *)

  constant x2: int
  constant y2: int
  axiom first_octant: 0 <= y2 <= x2

  (* The code.
      [(best x y)] expresses that the point [(x,y)] is the best
      possible point i.e. the closest to the real line (see the Coq file).
      The invariant relates [x], [y], and [e] and
      gives lower and upper bound for [e] (see the Coq file). *)

  use import int.Abs

  predicate best (x y: int) =
    forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)

  predicate invariant_ (x y e: int) =
    e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 /\
    2 * (y2 - x2) <= e <= 2 * y2

  lemma invariant_is_ok: forall x y e: int. invariant_ x y e -> best x y

  let bresenham () =
    let x = ref 0 in
    let y = ref 0 in
    let e = ref (2 * y2 - x2) in
    while !x <= x2 do
      invariant { 0 <= !x <= x2 + 1 /\ invariant_ !x !y !e }
      variant   { x2 + 1 - !x }
      (* here we would plot (x, y) *)
      assert { best !x !y };
      if !e < 0 then
        e := !e + 2 * y2
      else begin
        y := !y + 1;
        e := !e + 2 * (y2 - x2)
      end;
      x := !x + 1
    done

end
download ZIP archive