О схемах программ Схема проектирования цикла с помощью инварианта

Содержание ▲

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

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

Слайд 1

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

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

Слайд 2

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

Лекция 5 О схемах программ Схема проектирования цикла с помощью инварианта

Слайд 3

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

Схема программы (Котов В.Е., Сабельфельд В.К. Теория схем программ. М.: Наука, 1991 – 248 с.)

Слайд 4

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

Схема программы // вычисление n! (n0) p = 1; k = n; while (k !=0) { p = k *p; k = k  1; }

Слайд 5

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

Списки (напоминание)

Слайд 6

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

Модельное представление линейного списка

Слайд 7

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

Функция-конструктор Cons (x, y) Функция-конструктор Cons (x, y) x = a - элемент базового типа, y = (b c d e) - список Cons (x, y) = (a b c d e) Свойства: Cons ( Head (z), Tail (z)) = z Head(Cons (x, y)) = x Tail (Cons (x, y)) = y

Слайд 8

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

Иллюстрация Cons (Head (z), Tail (z)) = z

Слайд 9

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

Функция-конструктор Cons(x, y) Пустой список : ( ) или Nil Cons (a, Nil) = Cons (a, ( )) = (a) (a b c d e) = Cons (a, Cons (b, Cons (c, Cons (d, Cons(e, Nil))))) Это «операционное» представление списка Функция-индикатор: Null (z) Null (Nil) = true, z = (a b c d e)  Null (z) = false Всегда Null (Cons (x, y)) = false

Слайд 10

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

list p, k, n ; pp = Nil; kk = Nil; list p, k, n ; pp = Nil; kk = Nil; g(x) = Tail (x); h(x, y)= ConsHd (x,y)= Cons (Head (x), y); Null (x)  (x=Nil)

Слайд 11

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

Ручная прокрутка программы при n = (т о р г)

Слайд 12

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

// вычисление n! (n0) // вычисление n! (n0) p = 1; k = n; // inv: fct(k) *p = fct(n) // var: v (k)= k while (k !=0) { p = k *p; k = k  1; } // p =fct(n)

Слайд 13

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

Требования к инварианту и варианту цикла

Слайд 14

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

list p, k, n ; pp = Nil; kk = Nil; list p, k, n ; pp = Nil; kk = Nil; g(x) = Tail (x); h(x, y)= ConsHd (x,y)= Cons (Head (x), y); q (x,y) = Concat(x,y)