Given the following function f: int mystery(int x) //@requires....; //@ensures.....; //@ensures .....; { int r = 0; } int y = x; while (y > 1) //@loop_invariant .......; //@loop_invariant .......; { } y=y/2; r = r + 1; return r; use your skills for discovering what does it do, and write the correct contracts related to preconditions, postconditions and loop invariants. Show examples on how to test it on coin.