Разделы презентаций
- Разное
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Геометрия
- Детские презентации
- Информатика
- История
- Литература
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Задача о большинстве
Содержание
- 1. Задача о большинстве
- 2. Лекция 60. Задача о большинствеОб индивидуальных заданияхО
- 3. Об индивидуальных заданиях…21.04.2015О возможностях метода Хоара 1
- 4. О возможностях метода ХоараАбрамов С.А. Элементы анализа
- 5. Преамбула 21.04.2015О возможностях метода Хоара 1
- 6. 21.04.2015Аннотирование цикла и понимание аннотацийЦикл рекомендуется оформлять
- 7. 21.04.2015Список условий для проверки (аннотированного) цикла 1) показать,
- 8. 21.04.2015Пример: int i, n; //@ n > 0 i = 1; //@ inv P: (0
- 9. 21.04.20153) Утверждение !B есть (2*i > n). Отсюда очевидно, что (!B & inv) ≡ post (2*i > n) & (0
- 10. О переменных-призракахint i, n; //@ n > 0
- 11. Альтернатива – использование кванторовint i, n; //@ n > 0 i = 1; //@ inv P: (0
- 12. Соотношение между хоаровскими инвариантами цикла и индуктивными утверждениями ФлойдаСм. файлы .docx21.04.2015О возможностях метода Хоара 1
- 13. Скачать презентанцию
Лекция 60. Задача о большинствеОб индивидуальных заданияхО возможностях метода Хоара (Соотношение между хоаровскими инвариантами цикла и индуктивными утверждениями Флойда)21.04.2015О возможностях метода Хоара 1
Слайды и текст этой презентации
Слайд 2Лекция 6
0. Задача о большинстве
Об индивидуальных заданиях
О возможностях метода Хоара
(Соотношение между хоаровскими инвариантами цикла и индуктивными утверждениями Флойда)
метода Хоара 1
Слайд 4О возможностях метода Хоара
Абрамов С.А. Элементы анализа программ. Частичные функции
на множестве состояний. – М.: Наука. Гл. ред. физ.-мат. лит.,
1986.21.04.2015
О возможностях метода Хоара 1
Слайд 621.04.2015
Аннотирование цикла и понимание аннотаций
Цикл рекомендуется оформлять следующим образом:
//@ Pred
Q: предусловие
//@ inv P: инвариант
//@ bound t: ограничивающая функция
//@
(вариант цикла)while (B) {
S
}
//@ Post R: постусловие
Здесь Q – предусловие, а R − постусловие цикла, и выполняются соотношения Q → P, !B & P → R.
О возможностях метода Хоара 1
Из Лекции 2.2.(сл.31-34)
Слайд 721.04.2015
Список условий для проверки (аннотированного) цикла
1) показать, что P –
истинно до выполнения цикла, т. е. Q → P;
2) показать, что тело цикла
имеет свойство {B & P} S {P}, т. е. P – инвариант;3) показать, что !B & P → R;
4) показать, что P & B → (t > 0);
5) показать, что
{P & B} t1 = t; S; {0 ≤ t < t1},
т. е. t уменьшается на каждом шаге цикла.
инвариант
ограничивающая
функция
О возможностях метода Хоара 1
Из Лекции 2.2.(сл.31-34)
Слайд 821.04.2015
Пример: int i, n;
//@ n > 0
i = 1;
//@ inv P: (0
bound t: n − i while (2*i
5 указанных ранее условий.1) Очевидно {(n > 0) & (i = 1)} → inv.
2) Проверим свойство {B & inv} i = 2*i ; {inv}.
Очевидно (B & inv) ≡ {(2*i ≤ n) & (0 < i ≤ n)}.
Для оператора присваивания имеем:
{предусловие} i = 2*i ; {0
О возможностях метода Хоара 1
Из Лекции 2.2.(сл.31-34)
комментировать
Слайд 921.04.2015
3) Утверждение !B есть (2*i > n). Отсюда очевидно, что (!B &
inv) ≡ post
(2*i > n) & (0
Проверим свойство{0 < 2*i ≤ n} t1= n − i; i = 2*i; {0 ≤ t < t1}. Действительно,
{ wp } t1 = n − i; i= 2*i; {0 ≤ n − i < t1}
wp ≡ ( 0 ≤ n − 2*i < n − i )
(0 < 2*i ≤ n) → wp
Проверка завершена
О возможностях метода Хоара 1
Из Лекции 2.2.(сл.31-34)
Слайд 10О переменных-призраках
int i, n;
//@ n > 0
i = 1; // int j =
0; //@ inv P: (0
while (2*i <= n) i = 2*i ; // j = j + 1; //@ post: ( 0Альтернатива: см. след. слайд
21.04.2015
О возможностях метода Хоара 1
Слайд 11Альтернатива – использование кванторов
int i, n;
//@ n > 0
i = 1;
//@ inv
P: (0
//@ post: ( 0! Комментарии об усилении постусловия и т.п.
21.04.2015
О возможностях метода Хоара 1
Слайд 12Соотношение между хоаровскими инвариантами цикла и индуктивными утверждениями Флойда
См. файлы
.docx
21.04.2015
О возможностях метода Хоара 1
