Model-based testing

Доклад А.К. Петренко на конференции Яндекса 2011

http://video.yandex.ru/users/ya-events/view/383

Feedback

Курс окончен, всем спасибо! Если у Вас есть мысли, пожелания, мнения, нам будет интересно их выслушать. Не исключено, что мы в самом императивном смысле примем их во внимание ;)

Срочно! Проблемы с учебной частью

Просьба СЕГОДНЯ (20 января) подойти в учебную часть и разобраться с проблемами с ведомостями следующим студентам :

Куприк 527 группа
Творогов 524 группа

Завтра перед экзаменом это сделать будет нельзя, т.к. в учебной части никого не будет!

Разъяснение условия А3 по Флойду

Условие задания А3 по методам Флойда сформулировано недостаточно точно, на мой взгляд. я хочу пояснить формулировку этого задания.

Правила проведения пересдачи

Если вы захотите пойти на пересдачу, Ваши баллы, заработанные в семестре, делятся пополам. Пересдача проходит в том же формате, как и основной экзамен. Набранные на пересдаче баллы будут добавлены к половине набранных за семестр баллов и на основе границ 30-60-80 баллов будет выставлена оценка.

Список тем лекций

Советую, как минимум, иметь представление по каждому из вопросов из следующего списка (это краткий план материала лекций этого года), а лучше и знать формулировки и определения по каждому из вопросов. Фактически этот список можно воспринимать как список тем для теоретических вопросов на экзамене.

Показ работ третьей комиссии

состоится 19 января в 9:00 в аудитории 726. В 10:00 в П-14 состоится консультация к экзамену.

Экзамен

21 января состоится экзамен по нашему курсу. Начало в 9:00. У нас две аудитории: 520-524 группы пишут в П-5, остальные - в П-6. Экзамен письменный. Длительность 120 минут. Каждому студенту будет предложен билет, состоящий из 10 заданий. Задания покрывают весь курс лекций и семинаров. Каждое задание оценивается от 0 до 5 баллов. Список возможных типов заданий на экзамене можно скачать на странице курса. Ответы пишите прямо на билете. На экзамене можно пользоваться любой печатной продукцией и рукописными текстами (крайне рекомендуется взять конспекты лекций и пособия по нашему курсу). Пользоваться электронными средствами связи и всем прочим барахлом запрещается.

19 января в П-14 в 10:00 состоится консультация к экзамену. Вы сможете задать интересующие вас вопросы непосредственно лекторам курса.

Программа экзаменационного дня следующая:
9:00 - 11:00 - Вы пишете экзамен.
11:00 - 13:00 - мы проверяем Ваши работы.
13:00 - 14:00 - показ работ и выставление оценок в зачетки.

Если кто-либо согласен с имеющейся уже сейчас оценкой, подходите, пожалуйста, на проставление оценок в зачетки с 9 до 10 утра.

Третья комиссия состоится

18 января в ИСП РАН (ул. Александра Солженицына, дом 25). Начало в 9:30, а не в 9:00, как написано на доске 5 курса.

Показ работ второй комиссии состоится

13 января в 9:00. Аудитория 726.

Напоминаю, 19 января в 10:00 в П-14 будет консультация к экзамену.

Статья "Об одном примере нарушения принципа подстановки Лисков"

В мире не так много статей на русском языке, касающихся различных аспектов RAISE метода. Алексей Германович Пискунов регулярно пишет статьи по RAISE методу. Рекомендую ознакомиться с его статьей под названием "Об одном примере нарушения принципа подстановки Лисков". В том числе она будет полезна и при подготовке к экзамену. Рекомендую также почитать и другие статьи на странице Алексея Германовича.

Классические формальные методы разработки программ

Первым программистам приходилось писать программы в машинных кодах, и они мечтали о "программирующей программе", т.е. говоря современным языком, о программе-компиляторе с языка более высокого уровня, чем машинные коды. Мечты сбылись: были предложены удобные языки программирования высокого уровня и написаны компиляторы. Механическая работа по получению объектных кодов, эта рутинная работа, с успехом была автоматизирована ценой потери эффективности получаемого объектного кода, но зачастую эта цена ниже, чем цена поддержки исходных текстов: всё же работать с программами на языках высокого уровня куда эффективнее, нежели с машинными кодами.

Эта ситуация была уже 40-50 лет назад. С этого времени профессия программиста в этом плане сильно не изменилась. А тем не менее рутинная, механическая, работа осталась. Если у программиста в голове есть правильное понимание того, что должна делать программа, то пусть компьютер сам пишет программы, подчиняясь идеям программиста. Т.е. хотелось бы иметь "программирующую программу" нового поколения, которая по некому более высокоуровневому описанию, нежели теперешние широкоиспользуемые языки программирования, предлагала реализации, возможно ценой потери эффективности, но с бОльшими возможностями по поддержке программ в более высокоуровневом представлении.

В мечтах это представлялось следующим образом: подходит программист к доске, чертит на ней какие-то непонятные символы (это он кратко, но точно, описывает концепции, логику поведения, которая должна быть в программе. Затем, оформив это в виде файла, запускает некий "спец.транслятор", выдающий исходные тексты программы, выполняющие заданную программистом логику. Программист занимается человеческим делом, он думает о самой задаче (а ведь сейчас, согласитесь, задачи решаются сложные: попробуйте хотя бы представить объемы требований!). А рутинную работу человек уже не делает. Красиво, не правда ли!

А теперь вопрос, почему мы до сих пор так не программируем ?

Алгебраические аксиомы без предусловий

Это сообщение посвящено стилям написания аксиом для алгебраических спецификаций. Согласно синтаксису аксиома имеет следующий вид: all var : type :- bool_expr [pre bool_expr] (предусловие необязательно). А алгебраическая аксиома имеет вид: all var : type :- expr is expr [pre bool_expr] , где оба expr - это функциональные термы, предусловие необязательно. Идея алгебраического способа записи свойств состоит в том, чтобы всякие хитрые кванторы и логические связи выразить только при помощи композиций операций системы. Предусловие - по сути тоже использует логическую связку (импликацию), поэтому можно было бы пытаться выражать аксиомы без нее, т.е. без предусловий. Посмотрим, во что это выливается, как при этом меняется способ формулирования аксиом.

Ближайшие мероприятия

29 декабря, 10:00-11:00, показ работ первой комиссии, аудитория 726, проставление зачетов студентам АСВК, АЯ и СП
29 декабря, 14:00, Михаил Игоревич Петровский проставляет зачеты студентам АСВК, кто не сможет прийти к 10, но успешно прошел комиссию
...где-то в десятых числах января..... вторая комиссия
19 января, 10:00, консультация к экзамену (готовьте вопросы по формулировкам задач экзамена!), аудитория П-14
21 января, 9:00-11:00, экзамен, аудитории П-5 и П-6. Распределение студентов по аудиториям планируется объявить на консультации.

Формальные спецификации в проблематике совместимости hardware/software

Одной из областей, где действительно на практике используются людьми и приносят свои плоды формальные спецификации, является стандартизация интерфейсов. Если вы пишете небольшой софт, в нем небольшое число компонентов, ваша группа разработчиков сидит в одной комнате и, даже возможно, с заказчиком можно "говорить и показывать" буквально в реальном времени, то разработка не встречает тех проблем, которые возникают во всех остальных случаях. Большие, разнесенные на расстоянии, коллективы, масса унаследованного кода, сторонние организации (возможно, не имеющие отношения к разработке кода), требующие соблюдения международных стандартов (например, они хотят продавать заказанный ими вам софт зарубежом) - это приводит к плохой управляемости проектом. Тяжело найти одного-двух человек, которые бы взвалили на себя ношу владения всей ситуацией и принятие ответственных решений по координации действий всех участников проекта. Спасением в этой ситуации, как ни странно, является более строгий подход к деятельности, в том числе с ведением всевозможной документации. В частности, документации об интерфейсах компонентов, которые разрабатываются независимо, но должны в конечном счете "заработать вместе". Сказать - одно, а сделать - другое: то, что документация как-то будет использоваться, практически очевидно, но как это сделать эффективно? Действительно, эффективное управление крупными проектами - это сложная вещь, на ВМК ее не преподают, у нас факультет не инженерный и не менеджерский. Но вот то, что касается документации по интерфейсам, возникающие при этом задачи, которые приводят к моделям программ и требований, это, на мой взгляд, может быть интересно. Какие возникают проблемы с описанием интерфейсов? Говоря двумя словами, очень немногие умеют описывать интерфейсы четко. Последствия этого, я думаю, очевидны из предыдущих предложений. Одним из способов четкого описания является составление формализованных (или даже формальных) описаний интерфейсов. Что это, как это - отношу вас к статье "Использование формальных методов для обеспечения соблюдения программных стандартов", написанную в том числе лекторами нашего курса. Советую ознакомиться. В этой статье, на мой взгляд, много и теоретического, и фактологического полезного материала по тому, как на практике используются формальные спецификации. Кому нравится видеть материал в более компактном виде, могу посоветовать слайды Виктора Кулямина под названием "Формализация интерфейсных стандартов на практике".

Где взять оффлайновую версию Dafny

Если у вас Windows, идете на http://boogie.codeplex.com, жмете справа большую зеленую кнопку Download и скачиваете последнюю ночную сборку (на rise4fun.com всё ещё старая версия, содержащая ряд багов, в том числе обнаруженных нами). Остается распаковать ее и запустить оттуда Dafny.exe. Не уверен, что на x86 заработает - у меня x64 и всё запутилось без проблем. Если ругается на отсутствие Z3, то скачиваете его с сайта этого солвера: http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html - и ставите. У меня на x64 всё запустилось сразу.

Комиссия может быть 2,5 часа

Комиссия 28 декабря начнется не в 10:00, как было объявлено ранее, а в 9:00. Время окончания и аудитория не изменились - 11:30 в П-8. Таким образом, длительность комиссии - 2,5 часа. Всем удачи!

Источники незамкнутости алгебраической спецификации

Среди различных характеристик алгебраических спецификаций можно выделить следующие три важные характеристики:

• полнота
• непротиворечивость
• замкнутость

Полнота означает, что спецификация содержит описание всех нужных свойств. Непротиворечивость означает, что спецификация реализуема, существует программная система, обладающая всеми свойствами, перечисленными в спецификации. Замкнутость означает, что для каждой функциональной особенности (определенные данные, определенные ситуации) есть функция, которая создает эту функциональную особенность.

Эти характеристики нужны при проведении валидации спецификации. Это сообщение посвящено тому, как проверять спецификацию на замкнутость.

Проставление зачетов 26 декабря

для студентов кафедры АСВК - после 11:00 в аудитории 753.

для студентов кафедры СП - с 9:30 до 10:30 в аудитории 726.

для студентов кафедры АЯ - с 10:30 до 13:00 в МЗ-4 (с досдачей RSL для тех, кому это актуально).

Показ работ основного зачета состоится

26 декабря в 9:30 в аудитории 726 (кафедра системного программирования).