## 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.

**Authors:** Jean-Christophe Filliâtre

**Topics:** Non-linear Arithmetic

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

(* 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 (* [best x y] expresses that the point [(x,y)] is the best possible point i.e. the closest to the real line i.e. for all y', we have |y - x*y2/x2| <= |y' - x*y2/x2| We stay in type [int] by multiplying everything by [x2]. *) use import int.Abs predicate best (x y: int) = forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)

Key lemma for Bresenham's proof: if `b`

is at distance less or equal
than `1/2`

from the rational `c/a`

, then it is the closest such integer.
We express this property using integers by multiplying everything by `2a`

.

lemma closest : forall a b c: int. abs (2 * a * b - 2 * c) <= a -> forall b': int. abs (a * b - c) <= abs (a * b' - c) let bresenham () = let y = ref 0 in let e = ref (2 * y2 - x2) in for x = 0 to x2 do invariant { !e = 2 * (x + 1) * y2 - (2 * !y + 1) * x2 } invariant { 2 * (y2 - x2) <= !e <= 2 * y2 } (* here we would plot (x, y), so we assert this is the best possible row y for column x *) assert { best x !y }; if !e < 0 then e := !e + 2 * y2 else begin y := !y + 1; e := !e + 2 * (y2 - x2) end done end

download ZIP archive