I had this argument with a colleague some years back. He said that passing a reference to a variable directly is faster than passing a reference to a struct and then accessing a member of that struct. So I checked the assembly:
Thursday, August 20, 2020
Monday, August 3, 2020
Proof of function to normalize angles using why3
Problem: Write a function to normalize an angle to between -179 and 180 degrees (inclusive).
Solution (as found on StackOverflow here: https://stackoverflow.com/questions/2320986/easy-way-to-keeping-angles-between-179-and-180-degrees/2323034#2323034):
Proof (verify on http://why3.lri.fr/try/):
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.
Subscribe to:
Posts (Atom)