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 утра.
Есть вопрос по типовым заданиям. Методы Флойда, А2: "В блок-схеме программы выделена подсхема, в которую входит ровно одна дуга..."
ОтветитьУдалитьОт нас требуется написать полностью корректную "относительно некоторых условий" схему, гарантирующую достижимость В из А.
В точках А и В в общем случае разные оценочные функции. Поэтому непонятно, зачем эти функции вообще даны в условии - ведь они на достижимость В из А не влияют.
Непонятно, почему нельзя просто в ответе написать схему "skip" - чем это будет не отвечать заданным условиям?
Вы не учли условие наличия полной корректности с указанными оценочными функциями. Это означает, что, например, если оценочная функция в B тождественна 1, а в А - нулю, то B недостижима из А при наличии полной корректности. Это ответ на вопрос, как достижимость связана с оценочными функциями. Думаю, теперь очевидно, почему skip не подходит в том случае, если оценочные функции B и А не являются тождественными.
УдалитьЕще вопросы по типовым заданиям:
ОтветитьУдалитьФлойд, А7-А9
Почему а и д не подходят? Ведь по большому счету, условием может являться любое логическое выражение. Для любого наперед заданного логического выражения можно подобрать блок-схему, индуктивные утверждения, точки сечения, имена переменных так, чтобы данное выражение являлось, например, условием верификации.
И еще: Я правильно понимаю, что условие корректности - это условие верификации для пути, который заканчивается в HALT?
про А7-А9: я днем уточнил формулировку задания. Обратите, пожалуйста, внимание, сейчас она звучит так: "Что из перечисленного может быть ----тем-то---- ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)" Поэтому любое выражение теперь не подходит, а выражение должно иметь вид как в лекциях Алексея Хорошилова (с квантором всеобщности, с формулами пути, импликацией и всем прочим).
УдалитьПро условия корректности: нет, это совсем другое; условия корректности бывают двух видов: условия, что все частичные функции в программе вызываются с допустимыми аргументами, и условия, что каждый раз в точке сечения результат оценочной функции принадлежит фундированному множеству.
Спасибо. Я рассматривал старый вариант задания. Было бы здорово на сайте курса указать, что в примерах что-то изменилось.
УдалитьПро условие корректности тоже все ясно, спасибо.
Еще вопрос по типовым заданиям:
В RSL, A6 предлагается представить в виде аксиомы некоторую фразу естественного языка, правильно отразив её смысл. Каков критерий этой "правильности", если формальная семантика предложений естественного языка очевидно не может быть определена?
Критерий "правильности" - адекватность формальной записи обычному ("житейскому", среднестатистическому) пониманию фраз русского языка.
УдалитьИ последний вопрос: есть некоторое противоречие между http://mfsp-cmc.blogspot.com/2012/01/blog-post_355.html , где дана программа курса, и списком тем типовых заданий (RSL и RAISE, Флойд и аналит. верификация, инструмент PVS). Или "типы заданий на экзамене" - это не исчерпывающий список? Иными словами, будет ли на экзамене Danfy, Frama-C, Spec# и прочее, что есть в списке тем лекций, но чего нет в списке типовых заданий?
УдалитьНа экзамене будет материал не более чем в том объеме, который был прочитан на лекциях и показан на семинарах у студентов всех групп, поэтому Spec#, Dafny и Frama-C, раз они были только на лекциях, могут появиться лишь в теоретических вопросах. А большая часть остального материала - и в виде практических заданий.
УдалитьЕще вопрос по типовым заданиям. Методы Флойда, A3: Почему единственная точка сечения должна обязательно стоять перед входом во внутренний цикл? По-моему, она должна просто стоять на любой дуге, которая является общей для этих циклов. Это напрямую следует из того факта, что каждый цикл содежит точку сечения.
ОтветитьУдалитьВ ответе на пример для А3 не утверждалось, что это единственное место, где должна стоять точка сечения. Надо показать, что одной точки сечения всегда достаточно - это там и схематически показано.
УдалитьЗдравствуйте! Подскажите, пожалуйста, как трактовать цикл while true do skip end; в Флойде а1 -- он бесконечный, зачем он?
ОтветитьУдалитьЗдравствуйте! Он нужен для того, чтобы выполнялось определение частичной корректности: если уж программа завершилась, то постусловие должно быть в любом случае выполнено. Так что приходится "зацикливаться", если постусловие никак не может быть выполнено при данных, удовлетворяющих предусловию.
Удалить