module M (* Bresenham line drawing algorithm. *) use import int.Int use import module stdlib.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. *) logic x2 : int logic 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 logic best (x y:int) = forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2) logic invariant_ (x y e:int) = e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and 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 and x <= x2 + 1 and 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 (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/bresenham" End: *)