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

1991 – 248 с.)

// вычисление n!
p = 1; k = n;
while (k ≠ 0) {
p = k *p;
k = k − 1; 
}

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

Пример

14.04.2015

О схемах программ

программы:
p = pp; k = n;
while (k !=kk) {
p = h (k, p);
k = g (k);
}

Интерпретация схемы:
pp = 1; kk = 0; // константы
h(x, y) = x * y; g(x) = x – 1;

О схемах программ

d e) или [a, b, c, d, e] или (a; b; c; d; e)
Функции-селекторы: «голова» - head, first
«хвост» - tail, rest
применяются к непустому списку и позволяют разобрать его на составные части.
Например, Head (x) = a, Tail (x) = (b c d e),
Head (Tail (x)) = b, Tail (Tail (x)) = (c d e)

О схемах программ

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

О схемах программ

z

О схемах программ

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

О схемах программ

= Tail (x); h(x, y)= ConsHd (x,y)= Cons (Head (x), y);
Null (x) ≡ (x=Nil)
// Схема программы:
p = pp; k = n;
while (k !=kk) {
p = h (k, p);
k = g(k);
}

Интерпретация схемы в случае списков

// Программа:
//вход – список n, м.б. пустой
p = Nil; k = n;
while (k !=Nil) { // !Null(k)
p = ConsHd (k, p);
k = Tail (k);
}

Результат: ? Reverse (n)

14.04.2015

О схемах программ

//вход – список n, м.б. пустой
p = Nil; k = n;
while (k !=Nil) { // !Null(k)
p = ConsHd (k, p);
k = Tail (k);
}

О схемах программ

k
while (k !=0) {
p = k *p;
k = k − 1; 
} // p =fct(n)

// Схема программы:
// вычисление f(n)
p = pp; k = n;
// inv: q (f(k),p) = f(n)
// var: v (k) ***
while (k !=kk) {
p = h (k, p);
k = g(k);
} // p = f(n)

Интерпретация схемы: pp, kk – константы.
h(x, y) = x * y; g(x) = x – 1; q(x, y) = x * y;
Примечание: почему h(x, y) и q(x, y) разные функции

Добавим утверждения, т.е. спецификацию (предусловие, постусловие) + инвариант цикла

fct(n)=n!

О схемах программ

h(x, y) = x * y; g(x) = x – 1; q(x, y) = x * y;
При входе (p =pp) & (k =n) ⇒ q (f(k),p) = f(n)
Т.е. q (f(n),pp) =f(n)
При выходе (q (f(k),p)=f(n)) & (k =kk) ⇒ (p =f(n))
Свойство сохранения:
{(k !=kk) & (q (f(k),p) =f(n))}
p = h (k, p); k = g(k);
{(q (f(k),p) =f(n))}

14.04.2015

О схемах программ

= Tail (x); h(x, y)= ConsHd (x,y)= Cons (Head (x), y);
q (x,y) = Concat(x,y)

Интерпретация схемы в случае списков

// Программа: f(n)=Reverse(n)
//вход – список n, м.б. пустой
p = Nil; k = n;
// inv: q (f(k),p) = f(n)
// var: v (k)
while (k !=Nil) { // !Null(k)
p = ConsHd (k, p);
k = Tail (k);
} // p = f(n)

// Схема программы:
// вычисление f(n)
p = pp; k = n;
// inv: q (f(k),p) = f(n)
// var: v (k)
while (k !=kk) {
p = h (k, p);
k = g(k);
} // p = f(n)

14.04.2015

О схемах программ

(к а р т у з),
Concat (Nil,y) =y, Concat (x,Nil) =x
q (x,y) = Concat(x,y)
inv: q (f(k),p) = f(n)
т.е. Concat(Reverse(k),p) = Reverse(n)

Если ввести инфиксное обозначение
s1 ⊕ s2 = Concat (s1, s2),
то inv: Concat(Reverse(k),p) = Reverse(n) превратится в
Reverse(k) ⊕p = Reverse(n),
что легче интерпретировать как аналог
fct(k) *p = fct(n).

14.04.2015

О схемах программ

(k), p)

k

p

О схемах программ