Introducing Software Verification with Dafny Language: Představujeme ověřování softwaru pomocí jazyka Dafny: Prokazování správnosti programu

Recenze čtenářů

Aktuálně nejsou k dispozici žádné recenze čtenářů. Hodnocení je založeno na 2 hlasů.

Původní název:

Introducing Software Verification with Dafny Language: Proving Program Correctness

Obsah knihy:

Seznámíte se s ověřováním softwaru a dokazováním správnosti pomocí programovacího jazyka Dafny, který podporuje Microsoft Research. Zatímco některé jiné knihy na toto téma jsou poměrně matematicky přísné, tato kniha bude používat co nejméně matematických symbolů a přísnosti a každý pojem vysvětlí jednoduchou angličtinou. Je to ideální učebnice pro programátory a vývojáře se znalostí jazyka C# a dalších programovacích jazyků.

Napsat správný software může být obtížné, proto se seznámíte s koncepcí výpočtu a ověřováním softwaru. Poté tyto koncepty a techniky uplatníte, abyste mohli s jistotou psát kód bez chyb, který je snadno pochopitelný. Zdrojový kód bude k dispozici v průběhu celé knihy a je volně dostupný na GitHubu.

Po přečtení a použití této knihy budete schopni psát správný, velký svobodný zdrojový kód softwaru použitelný bez ohledu na to, jakou platformu a programovací jazyk používáte.

Co se naučíte

⬤ Objevte programovací jazyk Dafny podporovaný společností Microsoft Research.

⬤ Prozkoumejte Hoareovu logiku, imperativní a funkcionální programy.

⬤ Pracovat s předběžnými a následnými podmínkami.

⬤ Používat datové typy, porovnávání vzorů a třídy.

⬤ Ponořte se do ověřovacích příkladů pro potenciální opětovné použití ve vlastních projektech.

Pro koho je tato kniha určena

Vývojáři softwaru a programátoři, kteří mají alespoň základní zkušenosti s programováním. Není potřeba žádný specifický jazyk. Určeno i pro ty, kteří mají velmi základní matematické zkušenosti (funkce, proměnné).