Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs.