Lecture overview -- Keyboard shortcut: 'u'  Previous page: DBC and Programming Languages -- Keyboard shortcut: 'p'  Next page: Loop Invariants [Section] -- Keyboard shortcut: 'n'  Lecture notes - all slides and notes together  slide -- Keyboard shortcut: 't'  Help page about these notes  Alphabetic index  Course home  Page 30 : 32
Object-oriented Programming in C#
Contracts and Assertions
Code Contracts in C# 4.0

Code contracts in C# 4.0 is modelled after DBCTM in Eiffel

In addition, contract concepts are inspired from MS Spec#

Code contracts in C# is an afterthought - in contrast to Eiffel DBC which is a forethought

  • Code contract characteristics:

    • Conceptually similar to DBC in Eiffel.

    • Supplied via the class library - not the programming language.

    • Relies on static methods in class Contracts.

    • A binary rewritter patches the compiled C# code in order to enable and relocate assertions in the compiled assembly

    • A static contract checker is also supported

      • Based on assertions, the static contract checker attempts to prove program correctness