bresenham.mlw 1.51 KB
Newer Older
1
module M
2

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
3 4
(* Bresenham line drawing algorithm. *)

5
use import int.Int
6
use import module stdlib.Ref
7

8 9 10 11 12
(*  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.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
13
    [0 <= y2 <= x2]. The seven other cases can be easily
14
    deduced by symmetry. *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15

16 17
logic x2 : int
logic y2 : int
18
axiom First_octant : 0 <= y2 <= x2
19 20 21 22 23 24 25 26 27

(* 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

28
logic best (x y:int) =
29 30
  forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)

31
logic invariant_ (x y e:int) =
32
  e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
33
  2 * (y2 - x2) <= e <= 2 * y2
34

35
lemma Invariant_is_ok : forall x y e:int. invariant_ x y e -> best x y
36

37
let bresenham () =
38 39 40 41
  let x = ref 0 in
  let y = ref 0 in
  let e = ref (2 * y2 - x2) in
  while !x <= x2 do
42 43
    invariant {0 <= x and x <= x2 + 1 and invariant_ x y e }
    variant   { x2 + 1 - x }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44
    (* here we would plot (x, y) *) 
45
    assert { best x y };
46 47 48 49 50 51 52 53 54
    if !e < 0 then
      e := !e + 2 * y2
    else begin
      y := !y + 1;
      e := !e + 2 * (y2 - x2)
    end;
    x := !x + 1
  done

55
end
56 57 58

(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
compile-command: "unset LANG; make -C ../.. examples/programs/bresenham"
60 61
End: 
*)