Loop Verification with Invariants and Contracts.