Редактирование: МФСП: Оформление задач
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления. | Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления. | ||
- | == Задача 1 | + | == Задача 1== |
Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия. | Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия. | ||
+ | |||
+ | '''Важно''': в пост-условиях не должно быть локальных переменных | ||
'''Условие''': | '''Условие''': | ||
Строка 16: | Строка 18: | ||
===Комментарии=== | ===Комментарии=== | ||
- | + | Как любезно заметил [http://twitter.com/kornevgen/status/7015914018 kornevgen], дерево рисовать не обязательно:<blockquote>"@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"</blockquote> | |
- | + | ||
==Задача 2 (AX)== | ==Задача 2 (AX)== | ||
- | '''Комментарии''': | + | '''Комментарии''': если в сигнатуре функция определена на множестве ВСЕХ входных данных (потому что там -> а не -~->), то нельзя добавлять предусловие в описание функции -- необходимо это условие запихать в тело функции (т.е. если не удовлетворяет ему, то просто не меняется множество). |
- | + | ||
- | + | == Задача 5, метод Флойда== | |
- | + | ||
- | + | ||
- | + | ||
- | == Задача 5 | + | |
===Условие=== | ===Условие=== | ||
<pre> | <pre> | ||
Строка 45: | Строка 41: | ||
=== Решение === | === Решение === | ||
- | 1. Инвариант в B: P( | + | 1. Инвариант в B: P(x1, x2, y1, y2) is φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) '' // в условии не задан, придумываем сами'' |
Имеем 3 пути: | Имеем 3 пути: | ||
* S-B | * S-B | ||
- | :: ∀ | + | :: ∀ x1 ∀ x2 [(x1 >= 0) ∧ (x2 > 0) => φ(x1, x2) ∧ (x1 = x2*0 + x1) ∧ (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать ∧ (y1 = 0) ∧ (y2 = x1)'' |
* B-T-B | * B-T-B | ||
- | :: ∀ | + | :: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => φ(x1, x2) ∧ (x1 = x2*(y1+1) + (y2-x2)) ∧ ((y2-x2) >= 0)] |
* B-F-H | * B-F-H | ||
- | :: ∀ | + | :: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 < x2) => (x1 = x2*y1 + y2) ∧ (y1 < x2)] |
- | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция | + | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2. |
- | Условие корректности: ∀ | + | Условие корректности: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) => y2 <math>\isin</math> Nat] |
- | Условие завершимости: ∀ | + | Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ] |
=== Комментарии === | === Комментарии === | ||
- | + | Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
{{Курс МФСП}} | {{Курс МФСП}} |