Program Verification With Object Invariants On The Example Of Spec
Stc
Date: 2010-06-17
Time: 12:00
Room: BBL
BBL 023
Speaker: Joanna Gasiewska
Title: Program verification with object invariants on the example of Spec#
Abstract
Static verification is a powerful way to eliminate possible bugs in compile time.
Not only it automatically provides the specification to the code but also forces the
programmer to develop the correct applications. In object oriented programming the
most powerful way to achieve that is by using object invariants. Their major task is
to constrain the state stored in the object. In this talk I am going to present the
verification approach used in object oriented languages and the adjustments that has
to be made especially for these languages. I am going to present the state-of-art on
the example of the implementation that was made for .Net – Spec#.
