Задача о большинстве

Сентябрь 3, 2022

Главная
Алгебра
Задача о большинстве

Содержание

2. Лекция 6 0. Задача о большинстве Об индивидуальных заданиях О возможностях метода Хоара (Соотношение между хоаровскими
3. Об индивидуальных заданиях … 21.04.2015 О возможностях метода Хоара 1
4. О возможностях метода Хоара Абрамов С.А. Элементы анализа программ. Частичные функции на множестве состояний. – М.:
5. Преамбула 21.04.2015 О возможностях метода Хоара 1
6. 21.04.2015 Аннотирование цикла и понимание аннотаций Цикл рекомендуется оформлять следующим образом: //@ Pred Q: предусловие //@
7. 21.04.2015 Список условий для проверки (аннотированного) цикла 1) показать, что P – истинно до выполнения цикла,
8. 21.04.2015 Пример: int i, n; //@ n > 0 i = 1; //@ inv P: (0
9. 21.04.2015 3) Утверждение !B есть (2*i > n). Отсюда очевидно, что (!B & inv) ≡ post
10. О переменных-призраках int i, n; //@ n > 0 i = 1; // int j =
11. Альтернатива – использование кванторов int i, n; //@ n > 0 i = 1; //@ inv
13. Скачать презентацию

Слайд 2

Лекция 6
0. Задача о большинстве
Об индивидуальных заданиях
О возможностях метода Хоара (Соотношение

между хоаровскими инвариантами цикла и индуктивными утверждениями Флойда)

21.04.2015

О возможностях метода Хоара 1

Слайд 3

Об индивидуальных заданиях
…
21.04.2015
О возможностях метода Хоара 1

Слайд 4

О возможностях метода Хоара
Абрамов С.А. Элементы анализа программ. Частичные функции на

множестве состояний. – М.: Наука. Гл. ред. физ.-мат. лит., 1986.

21.04.2015

О возможностях метода Хоара 1

Слайд 5

Преамбула
21.04.2015
О возможностях метода Хоара 1

Слайд 6

21.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)

Слайд 7

21.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)

Слайд 8

21.04.2015
Пример: int i, n; //@ n > 0 i = 1; //@ inv P: (0 < i ≤ n) //@ bound

t: n − i while (2*i <= n) i = 2*i ; //@ post: ( 0

Проверим 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предусловие ≡ (0 < 2*i ≤ n) следует из (B & inv)

О возможностях метода Хоара 1

Из Лекции 2.2.(сл.31-34)

комментировать

Слайд 9

21.04.2015
3) Утверждение !B есть (2*i > n). Отсюда очевидно, что (!B & inv) ≡

post
(2*i > n) & (0 < i ≤ n) ≡ ( 0 4) t = n − i > 0 при 0 < 2*i ≤ n.
5) Проверим свойство
{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