procedure F(n: float) returns(r: float)
	ensures r == n;
{
	r := n;
}