Give a useful precondition, postcondition, loop invariant, and variant in Dafny.

method f(x0: int,y: int) returns (r: int) requires true ensures true { var x := x0; var d := 0; while x < y invariant true { x := x + 1; d := d + 1; } return d; }

method g(x: int) returns (r: int) requires true ensures true { var y := 0; var i := 0; while i < x invariant true { y := y + 2; i := i + 1; } return y; }

method h(x0: int, y0: int) returns (r: int) requires true ensures true { var x := x0; var y := y0; while x > 0 invariant true { x := x - 2; y := y + 1; } return y; }