bresenham.mlw 1.51 KB
 Jean-Christophe Filliâtre committed Dec 29, 2010 1 ``````module M `````` Jean-Christophe Filliâtre committed Mar 25, 2010 2 `````` `````` Jean-Christophe Filliâtre committed Mar 25, 2010 3 4 ``````(* Bresenham line drawing algorithm. *) `````` Jean-Christophe Filliâtre committed Dec 29, 2010 5 ``````use import int.Int `````` Jean-Christophe Filliâtre committed Dec 30, 2010 6 ``````use import module stdlib.Ref `````` Jean-Christophe Filliâtre committed Dec 29, 2010 7 `````` `````` Jean-Christophe Filliâtre committed Mar 25, 2010 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 committed Mar 25, 2010 13 `````` [0 <= y2 <= x2]. The seven other cases can be easily `````` Jean-Christophe Filliâtre committed Mar 25, 2010 14 `````` deduced by symmetry. *) `````` Jean-Christophe Filliâtre committed Mar 25, 2010 15 `````` `````` Jean-Christophe Filliâtre committed Mar 25, 2010 16 17 ``````logic x2 : int logic y2 : int `````` Jean-Christophe Filliâtre committed Mar 26, 2010 18 ``````axiom First_octant : 0 <= y2 <= x2 `````` Jean-Christophe Filliâtre committed Mar 25, 2010 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 `````` Andrei Paskevich committed Jun 24, 2010 28 ``````logic best (x y:int) = `````` Jean-Christophe Filliâtre committed Mar 25, 2010 29 30 `````` forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2) `````` Jean-Christophe Filliâtre committed Dec 29, 2010 31 ``````logic invariant_ (x y e:int) = `````` Jean-Christophe Filliâtre committed Mar 25, 2010 32 `````` e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and `````` Jean-Christophe Filliâtre committed Mar 26, 2010 33 `````` 2 * (y2 - x2) <= e <= 2 * y2 `````` Jean-Christophe Filliâtre committed Mar 25, 2010 34 `````` `````` Jean-Christophe Filliâtre committed Dec 29, 2010 35 ``````lemma Invariant_is_ok : forall x y e:int. invariant_ x y e -> best x y `````` Jean-Christophe Filliâtre committed Mar 25, 2010 36 `````` `````` Jean-Christophe Filliâtre committed May 11, 2010 37 ``````let bresenham () = `````` Jean-Christophe Filliâtre committed Mar 25, 2010 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 `````` Jean-Christophe Filliâtre committed Dec 30, 2010 42 43 `````` invariant {0 <= x and x <= x2 + 1 and invariant_ x y e } variant { x2 + 1 - x } `````` Jean-Christophe Filliâtre committed Mar 25, 2010 44 `````` (* here we would plot (x, y) *) `````` Jean-Christophe Filliâtre committed Dec 30, 2010 45 `````` assert { best x y }; `````` Jean-Christophe Filliâtre committed Mar 25, 2010 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 `````` Jean-Christophe Filliâtre committed Dec 29, 2010 55 ``````end `````` Jean-Christophe Filliâtre committed Mar 25, 2010 56 57 58 `````` (* Local Variables: `````` Jean-Christophe Filliâtre committed Mar 25, 2010 59 ``````compile-command: "unset LANG; make -C ../.. examples/programs/bresenham" `````` Jean-Christophe Filliâtre committed Mar 25, 2010 60 61 ``````End: *)``````