Пример
Необходимо написать спецификацию функции сортировки
Sort(A,N)
//сортировка массива
//предусловие: переменная А является массивом
//состоящим из N целых чисел, N>0
// постусловие: целые числа в массиве A упорядочены.
Sort(A,N)
Достаточно ли этих пред- и постусловий?
Очевидно, что нет:
Во-первых, не указано в каком порядке необходимо упорядочить числа
Во-вторых, не указано, насколько большим может быть число элементов в массиве N.
Пересмотренная
спецификация: Sort(A,N)
//сортировка массива в возрастающем порядке
//предусловие: переменная А является массивом
//состоящим из N целых чисел,1<=N<=MAX_N
//где MAX_N – глобальная константа //задающая максимальный размер массива А
//постусловие: целые числа в массиве A упорядочены
//по возрастанию: A[1]<=A[2]<= …<= A[N]
//число N не изменилось
В предусловии описываются входные аргументы функции, указываются все глобальные именованные константы, использующиеся в ней, перечисляются все ограничения, которые накладываются функцией.
В постусловии описываются результаты работы функции (либо возвращаемое функцией значение) и все последствия ее работы.
Этап 3. Верификация
Будем называть
диагностическим утверждением некоторое формальное высказывание, описывающее некоторые конкретные условия, которые должны выполняться в определенной точке программы
Этап 3. Верификация
Пример простых утверждений – это пред- и постусловия, которые должны выполняться соответственно в начале и в конце функции.
Этап 3. Верификация
Инвариант – это условие, которое должно всегда быть истинным в некоторой точке программы
Инвариант цикла – это условие, которое должно выполняться до и после каждого выполнения цикла.
использование инварианта цикла для
решения следующей задачи: вычислить сумму первых n элементов массива А
//вычисляет сумму элементов A[0],A[1], … A[n-1]
// для любого n>0 int j=0; sum=0; while (j<n)
{
sum+=A[j];
++j;
} // конец оператора while
Инвариант данного цикла: значение переменной sum равно сумме элементов A[0]+A[1]+ … +A[j-1], j – значение параметра цикла