Thursday, August 20, 2020

Passing struct and accessing member variable vs passing member variable directly, which is faster?

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:

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):
// 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.