bresenham.mlw 1.68 KB
 Jean-Christophe Filliâtre committed Mar 25, 2010 1 2 ``````(* Bresenham line drawing algorithm. *) `````` Jean-Christophe Filliatre committed Apr 03, 2011 3 ``````module M `````` Jean-Christophe Filliâtre committed Mar 25, 2010 4 `````` `````` Jean-Christophe Filliatre committed Apr 03, 2011 5 `````` use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 6 `````` use import ref.Ref `````` Jean-Christophe Filliatre committed Apr 03, 2011 7 `````` `````` Jean-Christophe Filliatre committed May 20, 2011 8 9 `````` (* Parameters. Without loss of generality, we can take [x1=0] and [y1=0]. `````` Jean-Christophe Filliatre committed Apr 03, 2011 10 `````` Thus the line to draw joins [(0,0)] to [(x2,y2)] `````` Jean-Christophe Filliatre committed May 20, 2011 11 `````` and we have [deltax = x2] and [deltay = y2]. `````` Jean-Christophe Filliatre committed Apr 03, 2011 12 13 14 15 `````` Moreover we assume being in the first octant, i.e. [0 <= y2 <= x2]. The seven other cases can be easily deduced by symmetry. *) `````` Jean-Christophe Filliatre committed Feb 06, 2012 16 17 `````` constant x2: int constant y2: int `````` Jean-Christophe Filliatre committed Jul 26, 2011 18 `````` axiom first_octant: 0 <= y2 <= x2 `````` Jean-Christophe Filliatre committed Apr 03, 2011 19 `````` `````` Jean-Christophe Filliatre committed May 22, 2013 20 21 22 23 `````` (* [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]. *) `````` Jean-Christophe Filliatre committed May 20, 2011 24 `````` `````` Jean-Christophe Filliatre committed Apr 03, 2011 25 `````` use import int.Abs `````` Jean-Christophe Filliatre committed May 20, 2011 26 `````` `````` Jean-Christophe Filliatre committed Jul 26, 2011 27 28 `````` predicate best (x y: int) = forall y': int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2) `````` Jean-Christophe Filliatre committed May 20, 2011 29 `````` `````` Jean-Christophe Filliatre committed May 22, 2013 30 31 32 `````` (** 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]. *) `````` Jean-Christophe Filliatre committed May 20, 2011 33 `````` `````` Jean-Christophe Filliatre committed May 22, 2013 34 `````` lemma closest : `````` Jean-Christophe Filliatre committed Feb 06, 2014 35 `````` forall a b c: int. `````` Jean-Christophe Filliatre committed May 22, 2013 36 37 `````` abs (2 * a * b - 2 * c) <= a -> forall b': int. abs (a * b - c) <= abs (a * b' - c) `````` Jean-Christophe Filliatre committed May 20, 2011 38 `````` `````` Jean-Christophe Filliatre committed Apr 03, 2011 39 40 41 `````` let bresenham () = let y = ref 0 in let e = ref (2 * y2 - x2) in `````` Jean-Christophe Filliatre committed May 22, 2013 42 43 44 45 46 47 `````` 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 }; `````` Jean-Christophe Filliatre committed Apr 03, 2011 48 49 50 51 52 `````` if !e < 0 then e := !e + 2 * y2 else begin y := !y + 1; e := !e + 2 * (y2 - x2) `````` Jean-Christophe Filliatre committed May 22, 2013 53 `````` end `````` Jean-Christophe Filliatre committed Apr 03, 2011 54 `````` done `````` Jean-Christophe Filliâtre committed Mar 25, 2010 55 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 56 ``end``