Solution (as found on StackOverflow here: https://stackoverflow.com/questions/2320986/easy-way-to-keeping-angles-between-179-and-180-degrees/2323034#2323034):

```
// reduce the angle
angle = angle % 360;
// force it to be the positive remainder, so that 0 <= angle < 360
angle = (angle + 360) % 360;
// force into the minimum absolute value residue class, so that -180 < angle <= 180
if (angle > 180)
angle -= 360;
```

Proof (verify on http://why3.lri.fr/try/):

`module NormalizeAngle`

use int.Int

use int.ComputerDivision

let normalize (a: int) : int

requires { true }

ensures { result > -180 /\ result <= 180 /\ mod (a - result) 360 = 0 }

=

let ref r = a in

r <- mod r 360;

r <- mod (r + 360) 360;

if r > 180 then r <- r - 360;

r

let main () =

normalize (270)

end

This proof proves that the return value from the function is indeed between -179 and 180 and furthermore that the result is congruent to the input modulo 360 (recall that a and b are congruent mod n if their difference is divisible by n), which means that they are equal.
## No comments:

## Post a Comment