Редактирование: МФСП: Оформление задач

Материал из eSyr's wiki.

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 45: Строка 45:
=== Решение ===
=== Решение ===
-
1. Инвариант в B: P(x<sub>1</sub>, x<sub>2</sub>, y<sub>1</sub>, y<sub>2</sub>) is &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) '' // в условии не задан, придумываем сами''
+
1. Инвариант в B: P(x1, x2, y1, y2) is &phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) '' // в условии не задан, придумываем сами''
Имеем 3 пути:
Имеем 3 пути:
* S-B
* S-B
-
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> [(x<sub>1</sub> >= 0) &and; (x<sub>2</sub> > 0) => &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*0 + x<sub>1</sub>) &and; (x<sub>1</sub> >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y<sub>1</sub> = 0) &and; (y<sub>2</sub> = x<sub>1</sub>)''
+
:: &forall; x1 &forall; x2 [(x1 >= 0) &and; (x2 > 0) => &phi;(x1, x2) &and; (x1 = x2*0 + x1) &and; (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y1 = 0) &and; (y2 = x1)''
* B-T-B
* B-T-B
-
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> >= x<sub>2</sub>) => &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*(y<sub>1</sub>+1) + (y<sub>2</sub>-x<sub>2</sub>)) &and; ((y<sub>2</sub>-x<sub>2</sub>) >= 0)]
+
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2) => &phi;(x1, x2) &and; (x1 = x2*(y1+1) + (y2-x2)) &and; ((y2-x2) >= 0)]
* B-F-H
* B-F-H
-
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> < x<sub>2</sub>) => (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>1</sub> < x<sub>2</sub>)]
+
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 < x2) => (x1 = x2*y1 + y2) &and; (y1 < x2)]
-
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y<sub>2</sub>.
+
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2.
-
Условие корректности: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) => y<sub>2</sub> <math>\isin</math> Nat]
+
Условие корректности: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) => y2 <math>\isin</math> Nat]
-
Условие завершимости: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> >= x<sub>2</sub>) => (y<sub>2</sub> > y<sub>2</sub>-x<sub>2</sub>) ]
+
Условие завершимости: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2) => (y2 > y2-x2) ]
=== Комментарии ===
=== Комментарии ===
Строка 68: Строка 68:
==Задача 6 (PVS)==
==Задача 6 (PVS)==
'''ГЛАВНОЕ'''! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.
'''ГЛАВНОЕ'''! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.
-
* [[МФСП, 12 лекция (от 26 ноября)|Пример, разбиравшийся на лекции]]
 
-
* [[http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc|Ещё пример от Алексея Хорошилова]]
 
- 
{{Курс МФСП}}
{{Курс МФСП}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Шаблоны, использованные на этой странице:

Личные инструменты
Разделы