Задача о большинстве - презентация, доклад, проект скачать

Содержание ▲

Вы можете ознакомиться и скачать презентацию на тему Задача о большинстве. Доклад-сообщение содержит 12 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1

Описание слайда:

ВЕРИФИКАЦИЯ ПРОГРАММ ДВС Лектор - С.А. Ивановский

Слайд 2

Описание слайда:

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

Слайд 3

Описание слайда:

Об индивидуальных заданиях …

Слайд 4

Описание слайда:

О возможностях метода Хоара Абрамов С.А. Элементы анализа программ. Частичные функции на множестве состояний. – М.: Наука. Гл. ред. физ.-мат. лит., 1986.

Слайд 5

Описание слайда:

Преамбула

Слайд 6

Описание слайда:

Аннотирование цикла и понимание аннотаций Цикл рекомендуется оформлять следующим образом: //@ Pred Q: предусловие //@ inv P: инвариант //@ bound t: ограничивающая функция //@ (вариант цикла) while (B) { S } //@ Post R: постусловие Здесь Q – предусловие, а R  постусловие цикла, и выполняются соотношения Q  P, !B & P  R.

Слайд 7

Описание слайда:

Список условий для проверки (аннотированного) цикла 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

Слайд 8

Описание слайда:

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

Слайд 9

Описание слайда:

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