Added contracts with --@requires and --@ensures