Added curly brackets around @pre, @post, and @invariant