Title: Program verification with object invariants on the example of Spec#
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#.