Реферат: Написание программ вычисления факториалов
6
5-я итерация
i£n®
6
120
6
Рис. 10.2.
Введение Pre и Post условий.
В зависимости от исходного значения п , мы будем иметь разное число итераций цикла и разные состояния. Итак, на основе сделанного, мы можем сделать вывод: всякий оператор в программе определяет переход из одного множества состояний в другое.
Мы уже умеем определять множество с помощью предикатов. Пусть Q и R - предикаты, определяющие множество состояний до выполнения оператора S и после выполнения оператора S соответственно.
Это записывается так:
{Q} S {R} .
Это преобразование множества Q во множество R и определяет семантику оператора S.
Определение 10.1. Предикат Q называется предусловием оператора S, а предикат R - постусловием оператора S, если
{Q} S {R} .
Например, оператор fctrl : =1 ; из строки 7 рис. 10.1, любое состояние вычислительного процесса перерабатывает в состояние, где fctrl=1, т.е.
QºT , а R ºfctrl =1.
Семантика оператора присваивания.
Наша задача определить семантику оператора присваивания в терминах множеств состояний. Это означает, что нам надо определить взаимосвязь пред и постусловий для оператора присваивания. Эту задачу мы рассмотрим применительно к простым переменным.
Определение 10.2. Обозначим wp(S,R) - предикат, определяющий множество всех состояний, для которых выполнение оператора S, обязательно заканчивается за конечное время и обязательно в состоянии, удовлетворяющем предикату R.
Пример 10.1.
Пусть S - это оператор присваивания
i : = i+1 ,
а R º i £ 1 , тогда
wp(i : = i+1 , i £ 1)=( i £ 0).
Действительно, выполнение i : = i+1 может завершиться в состоянии
i£ 1 только, если i было меньше или равно нулю. Как следует из свойства операции сложения, если i > 0 , то i+1 >1 .
Пример 10.2.
Множество состояний, определяемых предикатом wp(S,T) для некоторого оператора S, есть множество всех состояний, таких, что выполнение оператора S, начавшееся в одном из этих состояний, обязательно заканчивается.
Определение 10.3. Обозначим 
предикат, который получается из предиката R , если в нем заменить все свободные вхождения переменной x на выражение е .