e-mail: |
http:// |
Abstract
The use of various forms of contracts, like preconditions, are
increasingly receiving more attention within Microsoft.
This talk describes the design of Spec#, an experimental superset
of the language C#, including pre- and postconditions and object
invariants. Spec# gives rise to dynamic checks of contracts.
The contracts can also be checked statically using the automatic
checker Boogie. The talk also reports on some initial
experience and describes some difficult issues in the design.