Predstavujeme verifikáciu softvéru s jazykom Dafny: Dokazovanie správnosti programu

Recenzie čitateľov

Momentálne nie sú žiadne recenzie čitateľov. Hodnotenie je založené na 2 hlasoch.

Pôvodný názov:

Introducing Software Verification with Dafny Language: Proving Program Correctness

Obsah knihy:

Zoznámte sa s overovaním softvéru a dokazovaním správnosti pomocou programovacieho jazyka Dafny, ktorý podporuje Microsoft Research. Zatiaľ čo niektoré iné knihy na túto tému sú pomerne matematicky prísne, táto kniha používa čo najmenej matematických symbolov a prísnosti a každý koncept vysvetľuje jednoduchou angličtinou. Je to ideálna učebnica pre programátorov a vývojárov so znalosťou jazyka C# a ďalších programovacích jazykov.

Napísať správny softvér môže byť ťažké, preto sa naučíte koncepciu výpočtu a overovania softvéru. Potom tieto koncepty a techniky aplikujte, aby ste mohli s istotou písať kód bez chýb, ktorý je ľahko pochopiteľný. Zdrojový kód bude k dispozícii v celej knihe a je voľne dostupný prostredníctvom služby GitHub.

Po prečítaní a použití tejto knihy budete schopní písať správny, veľký slobodný zdrojový kód softvéru použiteľný bez ohľadu na to, akú platformu a programovací jazyk používate.

Čo sa naučíte

⬤ Objavte programovací jazyk Dafny podporovaný spoločnosťou Microsoft Research.

⬤ Preskúmate Hoareho logiku, imperatívne a funkcionálne programy.

⬤ Pracovať s predbežnými a následnými podmienkami.

⬤ Používať dátové typy, porovnávanie vzorov a triedy.

⬤ Ponorte sa do overovacích príkladov na potenciálne opätovné použitie vo vlastných projektoch.

Pre koho je táto kniha určená

Vývojári softvéru a programátori, ktorí majú aspoň základné skúsenosti s programovaním. Nie je potrebný žiadny špecifický jazyk. Je určený aj pre tých, ktorí majú veľmi základné matematické skúsenosti (funkcie, premenné).