Chapter: Methods and Contracts
This chapter introduces the concept of contract that is essential for the discussion of correctness. In conjunction with function contracts we also discuss quantification. We assume familiarity with first-order predicate logic and quantification but give a overview of the logic and the corresponding Slang notation.