Code Contracts - 1. díl
 x   TIP: Přetáhni ikonu na hlavní panel pro připnutí webu
Reklama
Reklama

Code Contracts - 1. dílCode Contracts - 1. díl

 

Code Contracts - 1. díl

Google       Google       22. 3. 2011       15 523×

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.

Reklama
Reklama

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
přepíšeme na disjunkci (negace A nebo B):
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;
}
Předchozí ukázka použití metody TryParsePositive by už měla projít statickou analýzou.

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 });
pak by skončila výjimkou NullReferenceException, protože v cyklu by se zavolala instanční metoda ToString na null referenci. Hodil by se nám právě velký kvantifikátor, abychom do kontraktu mohli napsat:
"pro každý prvek x z items platí x != null". 
Toho lze v Code Contracts docílit pomocí metody Contract.ForAll(kolekce, predikát) jako v následující ukázce.
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.

×Odeslání článku na tvůj Kindle

Zadej svůj Kindle e-mail a my ti pošleme článek na tvůj Kindle.
Musíš mít povolený příjem obsahu do svého Kindle z naší e-mailové adresy kindle@programujte.com.

E-mailová adresa (např. novak@kindle.com):

TIP: Pokud chceš dostávat naše články každé ráno do svého Kindle, koukni do sekce Články do Kindle.

2 názory  —  2 nové  
Hlasování bylo ukončeno    
1 hlas
Google
Autor studuje vysokou školu a pracuje jako programátor. Zajímá se především o věci okolo platformy .NET a verifikaci programů. Kromě toho rád hraje fotbal a leze na boulderu.
Web    

Nové články

Reklama
Reklama
Obrázek ke článku Umělá inteligence ve výrobním podniku

Umělá inteligence ve výrobním podniku

V tomto článku shrnuji základní poznatky z nasazení inteligentních systémů v podnikové praxi. Jejich aplikace přináší značné výhody ale i řadu úskalí při nevhodném použití.

Obrázek ke článku CeBIT 2017 přibližuje digitalizaci

CeBIT 2017 přibližuje digitalizaci

Umělá inteligence, drony, humanoidní roboty, autonomní systémy, internet věcí. Digitalizace mění rychlým tempem hospodářství, správu i společnost. Na veletrhu CeBIT 2017 bude možno zažít potenciály digitální transformace v celém řetězci tvorby hodnot a po všech stránkách se seznámit s digitálními tématy od disruptivních technologií až po kybernetickou bezpečnost.

loadingtransparent (function() { var po = document.createElement('script'); po.type = 'text/javascript'; po.async = true; po.src = 'https://apis.google.com/js/plusone.js'; var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(po, s); })();
Hostujeme u Českého hostingu       ISSN 1801-1586       ⇡ Nahoru Webtea.cz logo © 20032017 Programujte.com
Zasadilo a pěstuje Webtea.cz, šéfredaktor Lukáš Churý