В основе данного учебного пособия лежит курс лекций прочитанный автором на математико-механическом факультете СПбГУ. В пособии рассматриваются методы формальных спецификаций, основанные на тройках Хора, и методы дедуктивной верификации императивных программ, а также построенный на основе данных методов язык программирования со встроенными формальными спецификациями Spec#. Подробно рассматриваются основные возможности языка Spec# и системы программирования Spec#, предназначенной для работы с ним. Учебное пособие предназначено студентам, магистрантам и аспирантам, обучающимся по направлению подготовки 010500 - Математическое обеспечение и администрирование информационных систем и специализирующимся в области теоретической и практической информатики.
V osnove dannogo uchebnogo posobija lezhit kurs lektsij prochitannyj avtorom na matematiko-mekhanicheskom fakultete SPbGU. V posobii rassmatrivajutsja metody formalnykh spetsifikatsij, osnovannye na trojkakh Khora, i metody deduktivnoj verifikatsii imperativnykh programm, a takzhe postroennyj na osnove dannykh metodov jazyk programmirovanija so vstroennymi formalnymi spetsifikatsijami Spec#. Podrobno rassmatrivajutsja osnovnye vozmozhnosti jazyka Spec# i sistemy programmirovanija Spec#, prednaznachennoj dlja raboty s nim. Uchebnoe posobie prednaznacheno studentam, magistrantam i aspirantam, obuchajuschimsja po napravleniju podgotovki 010500 - Matematicheskoe obespechenie i administrirovanie informatsionnykh sistem i spetsializirujuschimsja v oblasti teoreticheskoj i prakticheskoj informatiki.
