Lecture overview -- Keyboard shortcut: 'u'  Previous page: Examples of preconditions and postconditions -- Keyboard shortcut: 'p'  Next page: Responsibilities and Contracts [Section] -- Keyboard shortcut: 'n'  Lecture notes - all slides and notes together  slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Help page about these notes  Alphabetic index  Course home  Page 8 : 32
Object-oriented Programming in C#
Contracts and Assertions
An Assertion Language

We need an assertion language in which to write preconditions, postconditions, and other assertions

We want to check the assertions when the program runs

  • A possible assertion language

    • Logical expressions - as in the programming language

    • Programmed assertions - via boolean functions of the programming language

      • Should be simple functions

      • Problems if there are errors in these

    • Universal ("for all...") and existential ("there exists...") quantifiers

      • Requires programming - iteration - traversal

      • It may be expensive to check assertions with quantifiers

    • Informal assertions, written in natural language

      • Cannot be checked

      • Much better than nothing

    • Special means of expression

      • old Expr - The value of the expression at the beginning of the operation

      • nochange - A simple way to state that the operation has not changed the state of the object