Ostatnio popełniłem post na temat co to jest Code Contracts i na czym to polega. Teraz stwierdziłem, iż przyda się kilka informacji na temat ich debugowania – w szczególności iż kod ma działać jak warunki pre i post i jak to zostało zorganizowane.

Żeby nie odkrywać ameryki na nowo, w tym celu wykorzystam przykłady zawarte w instalce CC, a które znajdują się w katalogu:

C:Program FilesMicrosoftContractsSamples

Na pierwszy ogień weźmy przykład Rational. Otwórzmy plik solution i zmodyfikujmy klasę Sample1 (plik Program.cs) by wyglądała tak:

class Sample1
{
    private static Rational r2;
 
    static void Main(string[] args)
    {
        var r1 = new Rational(10, 5);
 
        var r3 = r1 + r2;
        r3.Invert();
        Console.WriteLine(r3);
    }
}

Ustawmy break point na deklaracji zmiennej r3 i odpalmy aplikację w trybie debug (F5). Zaraz po uruchomieniu aplikacja zatrzyma się nam na naszej linijce i nie oglądając się za siebie klikamy F11 (step-into). Zostaniemy przekierowani do przeciążonego operatora + gdzie mamy definicję dwóch Requires sprawdzających czy aby na pewno nasze parametry, które dodajemy nie są null. Wciskamy dwa razy F11 i lądujemy na linijce, w której kontrakt nie powinien być spełniony:

Contract.Requires(b != null);

Jeżeli wciśniemy jeszcze raz F11 to pokaże się nam ładne okienko z błędem:

cc01 (1)

Jeżeli chcemy uzyskać więcej informacji, to też możemy to zrobić za pomocą View Details:

cc02 (1)

No dobrze, to był prosty przykład i dość zrozumiały. Ale widać, że debugowanie nam działa i to poprawnie, tak jak chcemy :)

Teraz zmodyfikujmy deklarację r2 tak by wyglądała następująco:

private static Rational r2 = new Rational(5, 1);

Wyłączmy stary break point i ustalmy nowy na:

r3.Invert();

Wciskamy F5, potem F11 i jesteśmy w metodzie Invert, która zamiast sprawdzać parametry wejściowe (bo ich nie ma), weryfikuje wynik zapytania. Jeżeli teraz wciśniemy F11, to zamiast przejść i sprawdzić to co ma zostać zwrócone przejdziemy od razu do linijki niżej:

cc03

Może się to wydawać dziwne, jednak jak dobrze pamiętamy, Ensures działa na końcu tuż przed wyjściem z metody i przeprowadza weryfikacje tak by stan końcowy był stanem akceptowalnym. Czyli jeżeli klikniemy teraz cztery razy F11 to wylądujemy na metodzie Ensures:

cc04 (1)

Specjalnie pokazuje okno Locals, by można było zauważyć iż Ensures jest wykonywane na końcu. Zanim jednak nastąpi wywołanie naszego Ensures, jak wciśniemy F11, zostaniemy przerzuceni do tak zwanej metody ContractInvariantMethod:

cc05

A dopiero po niej zostanie wywołane Ensures.

No dobrze, czyli możemy ładnie i przyjemnie debugować proste kontrakty, przy tym zachowując logiczny ciąg zdarzeń zgodnych z logiką Hoara – {P} C {Q}. A co z bardziej skomplikowanym przypadkami? Takimi jak dziedziczenie, interfejsy? W dziedziczeniu w końcu nie możemy przeciążyć Requires, to jak możemy to debugować?

Po co się zastanawiać, możemy to od razu sprawdzić. Otwieramy projekt Invariants, modyfikujemy kod w Program.cs tak by wyglądał następująco:

static void Main(string[] args)
{
    BasicBankAccount.BankAccount b = new BasicBankAccount.BankAccount();
    b.Deposit(10);
    WallStreet.WallStreetAccount w = new WallStreet.WallStreetAccount();
    w.Deposit(-5);
}

Ustawiamy brak point na b.Deposit(10); i uruchamiamy debug (F5). Przechodząc po kolei przez kroki zauważymy, że nasza metoda ContractInvariantMethod w klasie BankAccount zostanie wywołana i że kod zakończy się sukcesem. Dobrze, przerywamy debugowanie, otwieramy metodęDeposit od WallStreetAccount i zamieniamy ją na:

public override void Deposit(int amount)
{
    this.slushFund += amount;
    this.balance -= amount;
}

Zmieniamy break point z b.Deposit na w.Deposit i odpalamy debug. Przechodząc przez kod nie trudno nie zauważyć, że nagle nasze wszystkie kontrakty szlak trafił. NawetContractInvariantMethod nie jest wywoływana, a co dopiero mówić o Requires, którego nie możemy przeciążyć w Deposit :/ No dobrze, skąd wiemy, że nie możemy? Dodajmy referencje do projektu WallStreet dla Microsoft Contracts a następnie włączmy analizę run-time kontraktów i podmieńmy Deposit na taki kod:

public override void Deposit(int amount)
{
    Contract.Requires(amount > 0);
    this.slushFund += amount;
    this.balance -= amount;
}

Już przy buildzie dostaniemy informację:

cc06

Czyli jednak coś tam z tych kontraktów działa :) Ale nie wszystko tak jakbyśmy chcieli, albo tak jak ja bym chciał – jeżeli coś mi przeciąża daną metodę i nie mogę tam już umieścić kontraktu, to niech on go waliduje by default a nie tylko i wyłącznie wtedy kiedy wywołam polecenie:

base.Deposit(amount);

Miejmy nadzieję, że to zostanie poprawione w przyszłych wersjach programu :)

Podsumowując, czyli mamy wsparcie debugowania i go nie mamy. Mamy dla prostych konstrukcji, dla złożonych musimy wciąż stosować obejścia w postaci wywołania metody klasy bazowej. Pytanie pozostaje, czy to zostanie naprawione? Mam nadzieję, że tak IMHO skoro nie można przeciążyć Requires to także kontrakt powinien zostać wykorzystany. Choć tutaj pewnie będą pojawiać się sprzeczne opinie ;)