Глава 7. Окрестностное тестирование программ. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы. - презентация

1 Глава 7. Окрестностное тестирование программ

2 Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений int, SR, ptr Инверсное вычисление ura Окрестностный анализ nan Приложения метавычислений Иные методы Иные приложения [2] Л.В.Парменова «Метавычисления и их применения. Суперкомпиляция» [1] С.М.Абрамов «Метавычисления и их применения» Область возможных новых исследований Окрестностное тестирование Реализация нестандартных семантик Инверсное программиро- вание Методы метавычислений Структура курса

3 Глава 7. Окрестностное тестирование программ µ Основные понятия: расхождение реальной и желаемой функции программы, спецификация, верификация, тестирование, корректность и частичная корректность µ Шаг и процесс тестирования, тест (набор) успешный (вскрывает ошибку), критерий выбора тестов, свойства критериев (полнота, непротиворечивость, вычислимость). µ Структурные критерии тестирования и их критика µ Идея улучшения ситуации и шаги формализации идеи (метасистемные уровни)

4 Глава 7. Окрестностное тестирование программ µ Шаги и процесс окрестностного тестирования µ Свойства окрестностного тестирования (полнота, применимость к разным языкам) µ Решение в рамках окрестностного тестирования традиционных задач Выбор следующего теста Локализация ошибки при отладке Переход от отладки к тестированию Использование текстов спецификаций при тестировании непротиворечивость невычислимость

5 7.1 Tестированиe. Основные понятия µ Программа p на языке L=(P L, D L, S L ) определяет функцию программы p :: D -> D: (λd -> S L (p, d)) µ Возможно расхождение между желаемой и реальной функцией программы µ Спецификация описывает требования на допустимые входные данные для p и желаемые соотношения между входными данными и результатом.

6 7.1 Tестированиe. Основные понятия µ Пример спецификации: ps=(φ, ψ), где φ :: D -> Bool предусловиe, ψ :: D -> D -> Bool постусловиe. µ Определение [частичная корректность] µ p частично корректна относительно φ и ψ : d D( (φ d) & (терминируется p d * L res) ) (ψ d res)

7 7.1 Tестированиe. Основные понятия µ Пример спецификации: ps=(φ, ψ), где φ :: D -> Bool предусловиe, ψ :: D -> D -> Bool постусловиe. µ Определение [корректность] µ p корректна относительно φ и ψ : d D(φ d) (терминируется p d * L res) & (ψ d res)

8 7.1 Tестированиe. Основные понятия µ Как правило в теории тестирования рассматривают частичную корректность программ, в теории верификации оба вида корректности µ Когда спецификация задана формально, можно попытаться верифицировать p доказать корректность p как формальную теорему µ На практике доказывать программы бывает трудно, в этом случае прибегают к тестированию

9 7.2 Процесс тестирования программы µ Тестирование программы p: серия тестовых прогонов программы над тестами d i D, удовлетворяющими предусловию (φ d i ) µ После каждого тестового прогона p d i * res i проверяют истинность постусловия (ψ d i res i )

10 7.2 Процесс тестирования программы µ Пусть T n =[d 1,... d n ] набор тестов. Используют терминологию µ Тест d i пройден программой p неуспешно (d i неуспешный тест для программы p, d i вскрывает ошибку в p), если.... (Аналогично для T n ). µ Тест d i пройден программой p успешно (d i успешный тест для программы p), если.... (Аналогично для T n ).

11 7.2 Процесс тестирования программы µ Критерий выбора тестов Cr определяет, когда конечный набор тестов T n можно считать достаточным для тестирования p µ Пока ограничимся рассмотрением критериев Cr такого класса: Cr :: P -> TS -> Bool где ТS = [D]

12 7.2 Процесс тестиро- вания програм- мы Начало тестирования Выбор очередного теста d n Проверка предусловия φ d n True Выполнение программы p d n * res n False Ошибка в программе. ОТЛАДКА Проверка критерия Cr p T n Проверка постусловия ψ d n res n Тестирование завершено False True Тестирование завершено

13 7.3 Структурные критерии выбора тестов µ Среди критериев выбора тестов, использующих только информацию о наборе тестов и тестируемой программе, наиболее известными являются структурные критерии:

14 7.3 Структурные критерии выбора тестов µ Тестирование команд. Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности было обеспечено прохождение каждой достижимой команды данной программы

15 7.3 Структурные критерии выбора тестов µ Тестирование ветвей. Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности было обеспечено прохождение каждого реализуемого варианта ветвления для каждой команды ветвления в данной программе

16 7.3 Структурные критерии выбора тестов µ Тестирование путей. Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности было обеспечено прохождение каждого реализуемого пути в графе управляющей структуры блок- схеме данной программы с числом итераций циклов 0, 1 и 2.

17 7.3 Структурные критерии выбора тестов µ В силу неразрешимости проблемы распознания достижимости команды в программе структурные критерии невычислимы: Cr p [d 1,... d n ]

18 7.4 Свойства критериев выбора тестов µ В теории тестирования изучают следующие три свойства критериев выбора тестов: Полнота p с ошибкой T: (Cr p T) & (T вскрывает в p ошибку) Надежность (непротиворечивость): p T, T: (Cr p T) & (Cr p T) (T, T успешны для p)|| (T, T не успешны для p) Вычислимость Cr p T

19 7.4 Свойства критериев выбора тестов. Полнота µ Полнота. Критерий называют полным, если в случае наличия ошибки в программе существует набор тестов, удовлетворяющий данному критерию и раскрывающий ошибку

20 7.4 Свойства критериев выбора тестов. Надежность µ Непротиворечивость (надежность). Любые два набора тестов, удовлетворяющие критерию, должны быть одновременно успешными или неуспешными для данной программы

21 7.4 Свойства критериев выбора тестов. Вычислимость µ Простота проверки критерий должен «легко» проверяться, например, он должен быть вычислимым

22 7.4 Свойства критериев: недостижимы на практике 1. Структурные критерии не являются ни надежными, ни вычислимыми 2. Известно, что не существует полного непротиворечивого критерия, зависящего от набора тестов и программы Cr p [d 1,... d n ] надо учитывать спецификацию задачи! 3. Известно, что не существует вычислимого полного непротиворечивого критерия, зависящего от набора тестов, программы и спецификаций µ Умный, честный и партийный любые два свойства (или одно) из трех, но не все три!

23 7.4 Подмена свойств критериев «разрешимыми приближениями» µ Исследование полноты и надежности критериев на ограниченном классе программ и/или ограниченном классе ошибок Как правило, такому исследованию поддаются очень узкие классы программ и/или ошибок, которые трудно признать имеющими отношение к реальной практике программирования

24 7.4 Статистическая оценка «реальной» полноты/надежности µ Статистические исследования «реальной» полноты и надежности критериев Например, на выбранных из практики реальных программах с реальными ошибками

25 7.4 Числовая эвристическая оценка полноты тестирования µ Введение числовой эвристической оценки полноты тестирования вместо проверки невычислимого критерия Например, в системах тестирования, основанных на структурных критериях, оператору может выдаваться числовой коэффициент «процент проверенной части» программы

26 7.5 Критика структурных критериев µ Идея структурных критериев: изучение лабиринта побывать во всех комнатах, пройти все варианты ветвлений и все пути, чтобы получить полную информацию о лабиринте

27 7.5 Критика структурных критериев µ Можно предположить, что структурные критерии есть различные формализации неформального критерия выбора тестов: Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности была использована вся информация о графе управляющей структуры (блок-схеме) данной программы (7.1)

28 7.5 Критика структурных критериев µ Различные подходы к формализации фразы «использована вся информация о графе...» приводят к различным структурным критериям µ Недостатки: Явно ориентированы на классические императивные языки

29 7.5 Критика структурных критериев µ Цель тестирования проверка функции программы на совпадение с желаемой функцией, а полнота проверки определяется по полноте использования информации об управляющей структуре программы. Но разве функция программы полностью определяется только управляющей структурой программы? µ Мысленный эксперимент...

30 7.5 Критика структурных критериев µ Структурные критерии будут особенно ненадежны для программ, функция которых «в малой степени» определяется управляющей структурой программы.

31 function F(x: string): string; type state = (q0, q1,... ); { множество состояний автомата } const NewState: array[state, char] of state = (...constants...); OutputChar: array[state, char] of char = (...constants...); var i:integer; y:string; { результат } q:state; { тек.состояние автомата } begin q := q0; y := ; { пустая строка } for i:=1 to length(x) do begin y := y + OutputChar[q,x[i]]; q := NewState[q,x[i]]; end; F := y; end; Конечный автомат init … exit

32 7.6 Критика структурных критериев µ Анализ только управляющей структуры программы одна из возможных причин ненадежности структурных критериев µ Аппелляция к понятию «управляющая структура» ограничивает область применения критериев (только классические императивные языки)

33 7.6 Постановка проблемы. Неформальный предельный критерий µ Как исправить недостатки? µ Для оценки полноты тестирования надо анализировать то, что полностью определяет функцию программы: Текст программы целиком! то? что?

34 µ Было (надо поправить!) : Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности была использована вся информация о графе управляющей структуры (блок-схеме) данной программы (7.1) 7.6 Постановка проблемы. Неформальный предельный критерий

35 µ Набор тестов считается достаточным для тестирования программы, если в процессе тестовых прогонов на данном наборе в совокупности было обеспечено использование всей информации о полном тексте данной программы(7.2) µ Для формализации критерия 7.2 будет использован окрестностный анализ.

36 7.7 Метасистемные уровни в окрестностном тестировании µ «Что» использует информацию о тексте программы p в процессе тестовых прогонов? Переход от p d i * L res i к intL(p:d i ) * R res i

37 7.7 Метасистемные уровни в окрестностном тестировании µ «Что» использует информацию о тексте программы p в процессе тестовых прогонов? Переход от p d i * L res i к intL (p:d i ) * R res i

38 7.7 Метасистемные уровни в окрестностном тестировании µ Следующий шаг формализации определение понятия «использована информация», введение метасистемы, наблюдающей, как интерпретатор intL выполняет вычисление p d i и при этом потребляет информацию о p. Это окрестностный анализатор µ nan intL (p:d i ) * (res i, O (p:di) i )

39 7.7 Метасистемные уровни в окрестностном тестировании µ Метасистемные уровни (p:d) объекты, данные для intL intL система, выполняет вычисление p d i * res i nan метасистема, наблюдает, как работает система intL на данных (p:d), определяет, какая информация о данных (p:d) при этом используется системой intL

40 7.8 Шаг окрестностного тестирования µ Окрестностное тестирование последовательность (i=1,2,... ) вычислений: nan intL (p:d i ) * (res i, O i (p:di) ) decompose O i (p:di) [p] d i * (O i p, O i di ) Ō i p = O 1 p *O 2 p *...*O i p со следующими результатами на каждом шаге i:...

41 7.8 Шаг окрестностного тестирования µ со следующими результатами на каждом шаге i: res i результат R-вычисления intL (p:d i ) (или L-вычисления p d i * L res i ) O i (p:d i ) окрестность (p:d i ) информа- ционная интерпретация... O i p и Ō i p окрестности p информационная интерпретация... O i di окрестность d i информационная интерпретация...

42 7.8 Шаг окрестностного тестирования µ Заметим, что по определению Ō p k выполнено: Ō p 1 =O p 1 Ō p k+1 = Ō p k *O p k+1 k=1,2,... µ Ō p 1Ō p 2...Ō p kŌ p k+1... в данной последовательности окрестностей не может быть бесконечного числа отношений (>).

43 7.9 Окрестностный критерий выбора тестов µ Определение. Окрестность Ō p k неподвижная, если независимо от выбора теста d k+1 выполнено: Ō p k+1 = Ō p k µ Интерпретация. Если Ō p k неподвижная, то для любого d k+1 никакая новая информация о p не может быть использована в процессе вычислений p на тесте d k+1.

44 7.9 Окрестностный критерий выбора тестов µ Другими словами, eсли Ō p k неподвижная, то вся информация о p, которая необходима для проведения вычисления программы p на любых данных, была использована в тестовых прогонах программы p на тестах d 1,... d k

45 7.9 Окрестностный критерий выбора тестов µ Другими словами, eсли Ō p k неподвижная, то в тестовых прогонах p на тестах d 1,... d k была использована вся доступная информация о p. µ Определение. Окрестностный критерий тестирования: Набор (конечный список) тестов T k =[d 1,...d k ] будем считать достаточным для для тестирования программы p, если Ō p k является неподвижной окрестностью p.

46 7.10 Свойства окрестностного тестирования µ Теорема 19 Для любой программы p существует конечный набор тестов T, удовлетворяющий окрестностному критерию тестирования. µ Идея доказательства: рассмотрим любое перечисление множества dom(p) данных, на которых p терминируется...

47 7.10 Свойства окрестностного тестирования µ Теорема 20 Окрестностный критерий тестирования программ полный: в случае наличия ошибки в программе p существует конечный набор тестов T, раскрывающий ошибку и удовлетворяющий окрестностному критерию. µ Известно: не существует полного надежного (непротиворечивого) критерия, зависящего от набора тестов и программы.

48 7.10 Свойства окрестностного тестирования µ Далее будет показано, что критерий окрестностного тестирования программы p с заданной спецификацией ps не только полный, но и непротиворечивый. µ Следовательно, критерий окрестностного тестирования алгоритмически неразрешим. µ В общем случае окрестностный критерий тестирования должен проверяться экспертно.

49 7.10 Свойства окрестностного тестирования µ В некоторых случаях неподвижность Ō p k может быть очевидна. µ В остальных случаях полагаемся на то, что предлагаемые экспертам окрестности Ō p k имеют достаточно наглядную форму. µ Еще возможно ввести эвристическую числовую оценку близости окрестности Ō p k к неподвижной окрестности (на следующем слайде). µ Еще одно свойство: для окрестностного тестирования несущественны характеристики языка L

50 Расстояние между Ō p k > Ō p k+1 Ō p k+1 ŌpkŌpk ŌpkŌpk ρ(Ō p k, Ō p k+1 )= число разбиений

51 Числовая оценка близости окрестности Ō p n к неподвижной Ōp0Ōp0 Ōp1Ōp1 ŌpnŌpn Ōp2Ōp2 ÕpÕp Ō p ρ 0,n /ρ 0, ρ 0,n /ρ 0,~ ρ 0,1 ρ 1,2 ρ n, ρ o,n ρ 0, ρ 0,~ …

52 7.11 Традиционные проблемы тестирования µ Пусть успешно выполнено тестирование p для набора T n =[d 1,...,d n ], и критерий для T n не выполнен. Как выбрать следующий тест d n+1 ? µ Естественно, желаем продвижения в сторону выполнения критерия... µ Для структурных критериев проблема алгоритмически неразрешима. µ Если взять d n+1, где i [1..n], то получим текстуальное равенство результатов, трасс, окрестностей

53 7.11 Выбор очередного теста µ (p:d n+1 ) O (p:d i ) i tr(int, (p:d n+1 )) = tr(int, (p:d i )) µ p d n+1 = p d i = res i O (p:d n+1 ) n+1 = O (p:d i ) i O p n+1 = O p i Ō p n+1 = Ō p n µ В вычислении p на d n+1 не будет использовано никакой новой информации о p

54 7.11 Выбор очередного теста µ Вывод: d n+1 необходимо выбирать из следующего множества: µ \(... )=, где Q n = D p \[O d O d n n ] = [C Q C Q k n ] µ Разумно взять k n новых тестов, по одному из каждого C Q i i=1,... k n. µ Утверждение 21 Если =Ø, то Ō p n неподвижная окрестность.

55 7.11 Выбор очередного теста d1d1 d1d1 d2d2 d3d3 d4d4 d1d1 d2d2 d3d3 d4d

56 7.12 Традиционные проблемы тестирования. Тестирование и отладка. Локализация ошибки µ Предположим, что успешно пройден набор тестов T n и неуспешно тест d n+1. Программа p содержит ошибку. Где прежде всего следует ее искать? µ Предположим, что мы хотим сохранить не только результаты вычислений p d i =res i, но и трассы tr(int,(p:d i )) успешных тестовых прогонов на данных d 1,... d n. В таком предположении:

57 7.12 Тестирование и отладка. Локализация ошибки µ Исправленная программа p должна удовлетворять требованию p Ō p n µ Это означает, что исправления должны вноситься в надчеркнутые фрагменты в эксплицированной записи Ō p n µ С другой стороны, результат p d n+1 должен отличаться от неверного результата p d n+1 µ Таким образом, p, т.е. p \. Это еще больше локализует места возможных исправлений

58 7.12 Тестирование и отладка. Локализация ошибки µ В случае, если нет уверенности в необходимости сохранения трасс успешных прогонов на наборе T n, надо данную рекомендацию о местах внесения исправлений рассматривать как эвристику и начинать поиск ошибки именно с этих мест

59 7.13 Продолжение тестирования после исправления ошибки µ Предположим, что ошибка найдена, программа p исправлена, p новый текст программы. Нужно ли повторять все вычисления p на всех тестах d 1,... d n ? Или можно гарантировать, что на части тестов из T n программа p будет успешно работать? Как отобрать из T n эти тесты?

60 µ Если выполнено условие p, где i [1..n], то нет необходимости выполнять вычисление p на тесте d i. Действительно: µ p (p:d i ) tr(intL,(p:d i )) = tr(intL,(p:d i )) p d i = p d i = res i O (p:d i ) i =O (p:d i ) i O p i =O p i µ Таким образом, необходимо только пересчитать O d i i : decompose O (p:d i ) i [p] d i = (O p i, O d i i ) 7.13 Продолжение тестирования после исправления ошибки

61 µ В тех случаях, когда программа p достаточно сложная, указанная проверка p и пересчет O d i i займет значительно меньшее время, чем выполнение вычисления p на тесте d i Продолжение тестирования после исправления ошибки

62 7.14 Использование в тестировании спецификации µ Когда задана формальная спецификация программы, желаем основывать выбор тестов не только на анализе текста программы, но и на анализе текста спецификаций. µ Хотелось бы достичь формализации следующего критерия: на наборе тестов T n при проверке предусловий, тестовых прогонах и проверке постусловий должна быть использована вся информация о тексте программы и тексте спецификаций

63 µ Пусть S язык высокого уровня для написания спецификаций программ, φ предусловие, и ψ постусловие для p L, φ,ψ S одно и двухместный предикаты на D: (φ [d]) {True, False} (ψ [d, res]) {True, False} True, False два различных значения из D, intS R интерпретатор языка S, написанный на языке R Использование в тестировании спецификации

64 µ Процесс тестирования p с заданной спецификацией ps=(φ, ψ) можно рассматривать как процесс тестирования составной программы corr (φ, p, ψ) пунктирная граница на следующем слайде, с ожидаемой функцией: True на всей области D 7.14 Использование в тестировании спецификации

65 7.2 Процесс тестиро- вания програм- мы Начало тестирования Выбор очередного теста d n Проверка предусловия φ d n True Выполнение программы p d n * res n False Ошибка в программе. ОТЛАДКА Проверка критерия Cr p T n Проверка постусловия ψ d n res n Тестирование завершено False True Тестирование завершено

66 µ Будет удобно рассмотреть данную составную программу corr(φ,p, ψ) явно, как программу, написанную на некотором языке JobSL, являющемся надстройкой, языком заданий над языками S, L 7.14 Использование в тестировании спецификации

-} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res")" title="Программа corr(φ,p,ψ) на языке JobSL µ corr:: (S,L,S) -> JobSL corr(phi,p,psi)= (JOB [ Var"d" ] (ExecS phi [Var"d"] {-->-} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res")" class="link_thumb"> 67 Программа corr(φ,p,ψ) на языке JobSL µ corr:: (S,L,S) -> JobSL corr(phi,p,psi)= (JOB [ Var"d" ] (ExecS phi [Var"d"] {-->-} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res") (IF (Var "psi d res") -- THEN (EXIT (Const "True")) -- ELSE (EXIT (Const "False")) -- Error! ))) -- ELSE (EXIT (Const "True")) ))) -- End of JOB -} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res")"> -} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res") (IF (Var "psi d res") -- THEN (EXIT (Const "True")) -- ELSE (EXIT (Const "False")) -- Error! ))) -- ELSE (EXIT (Const "True")) ))) -- End of JOB"> -} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res")" title="Программа corr(φ,p,ψ) на языке JobSL µ corr:: (S,L,S) -> JobSL corr(phi,p,psi)= (JOB [ Var"d" ] (ExecS phi [Var"d"] {-->-} (Var"phi d") (IF (Var "phi d") -- THEN (ExecL p [Var"d"] {-->-} (Var"res") (ExecS psi [Var"d",Var"res"] {-->-} (Var"psi d res")">

68 Синтаксис конструкций языка JobSL µ job::=(JOB [jvar 1,... jvar n ] jterm) jterm::= (ExecS progS [ jexp 1,...,jexp n ] jvarjterm) |(ExecL progL [ jexp 1,...,jexp n ] jvarjterm) |(IF jexp jterm 1 jterm 2 ) |(EXIT e-exp) jvar::=(Var name) jexp::=jvar |(Const d ) jbind::=(jvar := d) jenv::=[jbind 1,... jbind n ] n0 progS S progL L d D

69 Вспомогательные функции интерпретатора языка JobSL µ instance Eq JBind where ((Var n1):=_) == ((Var n2):=_) = (n1==n2) mkJEnv :: [JVar] -> [D] -> JEnv mkJEnv jvs ds = zipWith (:=) jvs ds (+.) :: JEnv -> JEnv -> JEnv je1 +. je2 = nub (je2++je1) calcJExp :: JExp -> JEnv -> D calcJExp (Const d) je=d calcJExp (Var name) je=head [ d | ((Var n):=d)

70 Интерпретатор языка JobSL µ calcJExps :: [JExp] -> JEnv -> [D] calcJExps jexs je = map (\ jex -> calcJExp jex je) jexs intJobSL :: JobSL->[D]->D intJobSL jvs jt0) d = evalJ jt0 je0 where je0 = mkJEnv jvs d evalJ :: JTerm -> JEnv -> D evalJ (ExecS p jexs jv jt) je = evalJ jt je whereargs= calcJExps jexs je res= intS p args je= je +. [jv := res]

71 Интерпретатор языка JobSL µ evalJ (ExecL p jexs jv jt) je = evalJ jt je where args = calcJExps jexs je res = intL p args je = je +. [jv := res] evalJ (IF jex jt1 jt2) je = if ((calcJExp jex je) =="True") then evalJ jt1 je else evalJ jt2 je evalJ (EXIT jex) je = calcJExp jex je intL :: L->[D]->D описание интерпретатора языка L intS :: S->[D]->D описание интерпретатора языка S [D]->D --... описание интерпретатора языка L intS :: S->[D]->D --... описание интерпретатора языка S">

72 Окрестностное тестирование corr(φ,p,ψ) (1/2) µ nan intJobSL (corr(φ,p,ψ):d i * (res i,O i (corr(φ,p,ψ):d i ) ) µ decompose O i (corr(φ,p,ψ):d i ) [corr(φ,p,ψ)] d i = (O i corr(φ,p,ψ),O i d i ) µ Ō i corr(φ,p,ψ) = O 1 corr(φ,p,ψ) *O 2 corr(φ,p,ψ) *...*O i corr(φ,p,ψ) i=1,2... µ Единственным допустимым результатом является res i ="True" µ К тестированию corr(φ,p,ψ) применимы все предыдущиe результаты

73 Окрестностное тестирование corr(φ,p,ψ) (2/4) µ Текст corr(φ,p,ψ) включает в себя полный текст p и ps=(φ,ψ), вычисление corr(φ,p,ψ) d i в общем случае включает в себя проверку предусловия φ d i, вычисление программы p d i * res i и проверку постусловия ψ d i res i

74 Окрестностное тестирование corr(φ,p,ψ) (3/4) µ Набор T n =[d 1,...,d n ] будет считаться достаточным для тестирования p с заданной спецификацией ps=(φ,ψ), если на данных тестах в совокупности в процессах: проверок предусловий φ d i ; вычисления программы p d i ; проверок постусловий ψ d i res i ; µ была использована вся доступная информация о текстe программы p и о тексте спецификации ps=(φ,ψ)

75 Окрестностное тестирование corr(φ,p,ψ) (3/4) µ Теорема 22 Окрестностный критерий тестирования программы p с заданной спецификацией ps=(φ, ψ) является надежным. Пусть выполнено окрестностное тестирование программы corr(φ,p,ψ) на конечном наборе тестов T n, результаты всех тестовых прогонов res i ="True", i=1,... n и выполнен критерий окрестностного тестирования для набора тестов T n. µ Тогда, программа p частично корректна по отношению к предусловию φ и постусловию ψ.

76 Окрестностное тестирование corr(φ,p,ψ) (2/2) µ Следствие 23 Неразрешимость окрестностного критерия тестирования. Не существует алгоритма, который определяет, является ли окрестность Ō p n неподвижной

77 Обзор: Глава 7. Окрестностное тестирование программ µ Основные понятия: расхождение реальной и желаемой функции программы, спецификация, верификация, тестирование, корректность и частичная корректность µ Шаг и процесс тестирования, тест (набор) успешный (вскрывает ошибку), критерий выбора тестов, свойства критериев (полнота, непротиворечивость, вычислимость). µ Структурные критерии тестирования и их критика µ Идея улучшения ситуации и шаги формализации идеи (метасистемные уровни)

78 Обзор: Глава 7. Окрестностное тестирование программ µ Шаги и процесс окрестностного тестирования µ Свойства окрестностного тестирования (полнота, применимость к разным языкам) µ Решение в рамках окрестностного тестирования традиционных задач Выбор следующего теста Локализация ошибки при отладке Переход от отладки к тестированию Использование текстов спецификаций при тестировании непротиворечивость невычислимость