Visual Basicben nincsenek helyességbizonyítást támogató eszközök, ám a Code Contracts használatával lehetőségünk adódik kódunk ellenőrzésére.
Lehetőségünk van ellenőrizni, hogy egy adott feltétel teljesül-e a program adott pontján a Debug.Assert művelettel. Ez a művelet egy logikai kifejezést vár, amit kiértékelhet. Ha a kiértékelés igaz eredménnyel zárul, akkor a program folytatódik, ha viszont hamissal, akkor a program végrehajtása megáll.
A művelet gyengesége, hogy csak Debug módban fejti ki ezt a hatását, a lefordított kódban akkor sem történik semmi, ha a feltétel nem teljesül.
Az alábbi példa szemléltet egy lehetséges kezelést erre a proglémára.
Ekkor az alábbi használható a Debug.Assert helyett:
Ilyenkor az IDE-ben megáll a program, az EXE pedig hibát dob, ha a feltétel nem teljesült.
A Code Contracts lehetőséget nyújt elő- és utófeltételek, valamint objektum invariánsok megadására. Tartalmaz osztályokat a kódunk értékelésére, egy statikus elemzőt fordítás idejű analízishez, valamint egy futási idejű elemzőt. A CC osztályai a System.Diagnostics.Contracts namespace-ben találhatóak. A CC előnyel többek között:
Előfeltételek megfogalmazására a Contract.Requires metódus használatával van lehetőség, általában érvényes paraméterek ellenőrzésére használjuk. Az előfeltételben megadott összes tagnak legalább olyan láthatóságának kell lennie, mint magának a metódusnak.
Az alábbi kifejezéssel x szükségességét fogalmazhatjuk meg:
Contract.Requires( x != null );
Contract.Requires( x != null, "x" );
Az utófeltételek ellenőrzésére a metódusból való kilépés előtt kerül sor. Az előfeltételekkel szemben az utófeltételek kisebb láthatóságú tagokra is hivatkozhatnak.
A felhasználó lehet, hogy nem tudja értelmezni az információt amit egy 'private' állapotot használó utófeltételtől kap, ám ez nem befolyásolja a metódus helyes használatában.
Standard utófeltételek:
Standard utófeltételek kifejezésére az Ensures metódus használatával van lehetőségünk. Utófeltételre egy példa alább látható.
Contract.Ensures( this .F > 0 );
Contract.EnsuresOnThrow( this.F > 0 );
Contract.OldValue<’e típusa’>(e)
Contract.OldValue(Contract.Result() + x) // ERROR
Az objektum invariánsok olyan feltételek, amelyeknek mindig igaznak kell lenniük az adott osztály összes példányára, amikor az objektum elérhető a felhasználó által.
Olyan feltételeket fogalmaznak meg, amelyek meghatározzák, hogy egy objektumot mikor tekintünk helyesnek.
Az invariáns metódusokat a ContractInvariantMethodAttribute attribútummal jelöljük. Ezek legfeljebb az invariáns metódusra vonatkozó hívások szekvenciáját tartalmazhatják.
Példa:
[ContractInvariantMethod] protected void ObjectInvariant () { Contract.Invariant ( this.y >= 0 ); Contract.Invariant ( this.x > this.y ); ... }
Imports System Imports System.Diagnostics.Contracts ' Az IArray objektumok rendezett halmaza._ Public Interface IArray 'Az Item property metódusokat kínál a tömb elemeinek olvasására, szerkesztésére. Default Property Item(ByVal index As Integer) As [Object] ReadOnly Property Count() As Integer ' Hozzáadunk egy elemet a listához. ' A visszatérési érték az a pozíció, ahová az új elemet beszúrtuk Function Add(ByVal value As Object) As Integer ' A lista összes elemének eltávolítása. Sub Clear() ' Elem beszúrása a tömbbe a megadott indexre. ' Az indexnek nemnegatívnek kell lennie, továbbá legfeljebb annyi ' lehet, ahány elem van a tömbben. Ha az index annyi, ahány elem van a ' tömbben, az érték a végére fűződik. Sub Insert(ByVal index As Integer, ByVal value As [Object]) ' Adott indexű elem kivétele. Sub RemoveAt(ByVal index As Integer) End Interface 'IArray _ Friend MustInherit Class IArrayContract Implements IArray Function Add(ByVal value As Object) As Integer Implements IArray.Add ' Visszaadja az indexet ahová az elemet beszúrtuk. Contract.Ensures(Contract.Result(Of Integer)() >= -1) Contract.Ensures(Contract.Result(Of Integer)() < CType(Me, IArray).Count) Return 0 End Function 'IArray.Add Default Property Item(ByVal index As Integer) As Object Implements IArray.Item Get Contract.Requires(index >= 0) Contract.Requires(index < CType(Me, IArray).Count) Return 0 End Get Set(ByVal value As [Object]) Contract.Requires(index >= 0) Contract.Requires(index < CType(Me, IArray).Count) End Set End Property Public ReadOnly Property Count() As Integer Implements IArray.Count Get Contract.Requires(Count >= 0) Contract.Requires(Count <= CType(Me, IArray).Count) Return 0 End Get End Property Sub Clear() Implements IArray.Clear Contract.Ensures(CType(Me, IArray).Count = 0) End Sub 'IArray.Clear Sub Insert(ByVal index As Integer, ByVal value As [Object]) Implements IArray.Insert Contract.Requires(index >= 0) Contract.Requires(index <= CType(Me, IArray).Count) ' Hogy közvetlen a végére szúrhassunk be. Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) + 1) End Sub 'IArray.Insert Sub RemoveAt(ByVal index As Integer) Implements IArray.RemoveAt Contract.Requires(index >= 0) Contract.Requires(index < CType(Me, IArray).Count) Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) - 1) End Sub 'IArray.RemoveAt End Class 'IArrayContract