Code Contracts - 1. díl

V dalším dílu krátkého seriálu o Code Contracts se podíváme podrobněji na post-conditions a ukážeme si, jak vztáhnout kontrakt i na výstupní parametry metod a na kolekce.

Code Contracts je možné stáhnout na stránkách Microsoft Dev Labs. Informace o výběru vhodné edice a o instalaci Code Contracts naleznete v úvodním dílu seriálu. Code Contracts si dokonce můžete vyzkoušet online.

Další možnosti post-conditions

Už v minulém článku jsem použil v post-condition "odkaz" na návratovou hodnotu. Jednalo se o následující kód.

public static Fractional FromInt(int i)
{
	Contract.Ensures(Contract.Result<Fractional>() != null);
	// ...

Důležité je uvědomit si, že v post-condition můžeme testovat i jiné věci než jen návratovou hodnotu. Například konstruktor třídy Fractional bychom mohli upravit takto:

public Fractional(int numerator, int denominator)
{
	Contract.Requires(denominator != 0);
	Contract.Ensures(this.Denominator == denominator);
	Contract.Ensures(this.Numerator == numerator);
	this.Numerator = numerator;
	this.Denominator = denominator;
}

Co tím získáme? "Okolnímu světu" sdělíme, na co se po zavolání konstruktoru může spolehnout (vlastnosti Numerator a Denominator budou mít hodnoty odpovídající parametrům), a navíc nám statický analyzátor zkontroluje, že tomu tak opravdu je. Uvažme, že se v konstruktoru objeví následující chyba, která může snadno vzniknout obyčejnou nepozorností.

public Fractional(int numerator, int denominator)
{
	Contract.Requires(denominator != null);
	Contract.Ensures(this.Denominator == denominator);
	Contract.Ensures(this.Numerator == numerator);
	this.Numerator = numerator;
	this.Denominator = numerator; 
	// ^ opravdu jsem chtěl do Denominator přiřazovat numerator?
}

Pokud použijeme uvedené post-conditions, Code Contracts zkontrolují, zda je kód v konstruktoru "správně", upozorní nás na případné chyby a už není třeba psát pro takový konstruktor unit-testy.

Výstupní parametry v post-conditions

Výstupní parametry se často používají, když chceme z metody "vrátit" více výsledků. Příkladem mohou být známé metody TryParseXXX(string, out XXX). V takovém případě bychom chtěli uvést kontrakt nejen pro formální návratovou hodnotu, ale i pro výstupní parametr. Jak takovou věc provést si předvedeme na metodě TryParsePositive, která, podobně jako int.TryParse, naparsuje celé číslo z řetězce, ale rozdíl je v tom, že vrátí true, pouze pokud je daný řetězec validním zápisem čísla a navíc větším jak nula. Kód metody, zatím bez kontraktů, by mohl vypadat následovně.

public bool TryParsePositive(string input, out int num)
{
	return int.TryParse(input, out num) && num >= 0;
}

Co tedy budeme chtít v post-condition "okolnímu světu" oznámit? Pokud metoda vrátí true, pak se můžeme spolehnout, že num je větší nebo rovno nule. Ještě než přidáme potřebný kontrakt, pojďme se podívat, co by nám statický analyzátor řekl na následující kus kódu.

int i;
if (TryParsePositive("5", out i))
{
    string s = "ahoj svete";
    if (i < s.Length)
    {
        Console.WriteLine(s.Substring(i));
		// Code Contracts nám na předchozím řádku nahlásí, 
		// že i může být menší než nula, což by způsobilo 
		// výjimku IndexOutOfRange
    }
}

Jak už víme, metoda Substring obsahuje pre-condition, jež nám přikazuje předat jako první parametr číslo, které je menší než délka řetězce (to je ošetřeno pomocí ifu) a zároveň nesmí být záporné a to už v uvedeném kódu není nijak ošetřeno. Code Contracts neví nic o výstupním parametru TryParsePositive a nemohou vědět, že v tomto případě záporný být nemůže. Takže nám nezbývá než Code Contracts napovědět pomocí zmíněné post-condition.

"Pokud TryParsePositive vrátí true, pak je num >= 0" je výrok ve formě implikace. Code Contracts bohužel implikace přímo neumí, takže budeme muset zavzpomínat na základy logiky a vzpomenout si, že implikace "když A, pak B" (značení A -> B) je to samé jako "neplatí A nebo platí B" (disjunkce).

Ještě než se pustíme do zápisu výsledného kontraktu, je potřeba vědět, jak se odvolat na výslednou hodnotu parametru num. Statická třída Contract nabízí metodu ValueAtReturn. Její použití je podobné jako u metody Result.

Nyní už víme vše potřebné: implikaci

Contract.Result<bool>() -> Contract.ValueAtReturn<int>(out num) >= 0

public bool TryParsePositive(string input, out int num)
{
	Contract.Ensures(Contract.Result<bool>() == false ||
		Contract.ValueAtReturn<int>(out num) >= 0);
	return int.TryParse(input, out num) && num >= 0;
}

Volání pomocných metod v kontraktu

Možná některé z vás při čtení předchozích odstavců napadlo, že by bylo hezké udělat si pro implikaci pomocnou funkci. Význam logického výrazu by byl více zřejmý, což by měl být jeden z hlavních cílů při psaní udržovatelného kódu. Předchozí metodu bychom mohli upravit takto:

public static class ContractExtensions
{
	public static bool Implication(bool a, bool b)
	{
		return (a == false) || b;
	}
}

// ...
public bool TryParsePositive(string input, out int result)
{
	Contract.Ensures(
		ContractExtensions.Implication(
			Contract.Result<bool>(), 
			Contract.ValueAtReturn<int>(out num) >= 0));

Pokud ale tento kód zkusíme přeložit, Code Contracts nás upozorní, že metoda Implication nemá atribut [Pure]. Pokud nějakou metodu odekorujeme atributem [Pure], říkáme tím Code Contracts, že nemá vedlejší efekty. Vedlejším efektem je změna stavu nějakého objektu nebo interakce s "vnějším světem". Například Math.Sqrt vedlejší efekty nemá, zatímco Array.Sort zpřehází prvky zadaného pole, což je vedlejší efekt, stejně tak Console.WriteLine vypíše novou řádku, což je příklad interakce s "okolním světem". Proč po nás chtějí Code Contracts pouze metody bez vedlejších efektů? Například následující kód bude fungovat, pouze pokud budou Code Contracts zapnuté.

public static bool Sort(int[] array)
{
	Array.Sort(array);
	return true;
}

public bool Find(int[] array, int value)
{
	Contract.Requires(Array.Sort(array))
	
	// ... nějaký kód, který se spoléhá na to, že array je setříděné	

Bohužel statický analyzátor Code Contracts už nedokáže zpracovat pomocné metody, nicméně při jejich použití nám zůstává alespoň kontrola kontraktu za běhu, o které si povíme víc v jednom z následujících dílů.

Kvantifikace

Code Contracts souvisí se světem formální logiky, a tak se tu objevuje další pojem známý z tohoto odvětví. Kvantifikace jsou dvě, a to "pro každé x platí..." (velký kvantifikátor) a "existuje x takové, že..." (malý kvantifikátor).

Můžete si sami zkusit odhadnout, jaký problém naleznou Code Contracts v následující metodě.

public string Concat(IEnumerable<object> items)
{
	Contract.Requires(items != null);
	var sb = new StringBuilder();
	foreach(var item in items)
	{
		sb.AppendLine(item.ToString());
	}
	
	return sb.ToString();
}

Problematické je volání item.ToString(), pokud bychom metodu zavolali takto:

Concat(new object[] { null });

"pro každý prvek x z items platí x != null". 

public string Concat(IEnumerable<object> items)
{
	Contract.Requires(items != null);
	Contract.Requires(Contract.ForAll(items, x => x != null));
	// ... implementace zůstává nezměněna
}

Podobným způsobem lze použít i metodu Contract.Exists(kolekce, predikát).

Závěr

V dnešním díle jsme se podívali na pokročilejší možnosti použití Code Contracts, jmenovitě post-condition pro parametry s modifikátorem out, kvantifikátory a použití pomocných metod v kontraktu. V příštím díle se podíváme na specifikaci kontraktů pro rozhraní (interface) a abstraktní metody.