Ужин с ПК. Математика в тестировании

Андрей Ершов, Виталий Брагилевский, Дарья Манухина, Иван Пономарёв

Нужна ли математика в тестировании?

«Стать тестировщиком за три дня»

beatester
hh

Многие общематематические концепции переходят в практику

  • «Техника анализа классов эквивалентности»

\[\huge \begin{array}{lll} a \sim a \\ a \sim b \Rightarrow b \sim a \\ a \sim b \wedge b \sim c \Rightarrow a \sim c\\ [a]=\{\,x\in X\mid x\sim a\,\} \end{array}\]

Комбинаторика

  • Дано: чистая функция с тремя булевскими параметрами.

  • Вопрос: Сколько тест-кейсов надо написать, чтобы полностью протестировать эту функцию?

\[\huge 2^3 = 8\]

Комбинаторика

  • Дано: чистая функция с параметром в виде строки в алфавите \(a\) длиной не больше \(m\)?

  • Вопрос: Сколько тест-кейсов надо написать, чтобы полностью протестировать эту функцию?

\[\huge 1 + a + a^2 + \ldots + a^m = \frac{a^{m+1}-1}{a-1}\]

Комбинаторика

  • Дано: три браузера, три ОС, три сценария.

  • Вопрос: так сколько нам нужно тестов? и каким количеством тестов мы готовы обойтись?

latin3

Что почитать-посмотреть

Статистика

  • Дано: Из мониторинга мы взяли ~1 млн замеров latency за период \(А\) и ещё ~1 млн замеров latency за период \(B\).

  • Вопрос: Как понять, стала ли система работать лучше/хуже/ничего не изменилось?

datasaur
1. Datasaurus Dozen, https://www.autodesk.com/research/publications/same-stats-different-graphs

Что посмотреть?

Узнаем больше про статистику с Анатолием Карповым:
https://stepik.org/course/76/promo

stepik

Доклады (для тех, кто уже разбирается в статистике)

Логика

Что это такое?

\[\huge \forall n \in \mathbb{N}\;(L(n) \iff ( n \vdots 16) \vee (n \vdots 4 \wedge \neg n \vdots 25))\]

Является ли \(n\) номером високосного года в Григорианском календаре

Что посмотреть?

philosophers

Алгоритм dining_philosophers

algorithm dining_philosophers
  variables chopsticks = [chopstick \in 1..NP |-> NULL]
  define
    LeftChopstick(p) == p
    RightChopstick(p) == IF p = NP THEN 1 ELSE p + 1
    HeldChopsticks(p) == { x \in {LeftChopstick(p), RightChopstick(p)}: chopsticks[x] = p}
    AvailableChopsticks(p) == { x \in {LeftChopstick(p), RightChopstick(p)}: chopsticks[x] = NULL}
  end define;
  process philosopher \in 1..NP
  variables hungry = TRUE;
  begin P:
    while hungry do
      with chopstick \in AvailableChopsticks(self) do
        chopsticks[chopstick] := self;
      end with;
      Eat:
      if Cardinality(HeldChopsticks(self)) = 2 then
        hungry := FALSE;
        chopsticks[LeftChopstick(self)] := NULL ||
        chopsticks[RightChopstick(self)] := NULL;
      end if;
    end while;
  end process;
end algorithm;

TLA+

tlaplus

Model Checking

tla deadlock

Нужны ли тесты, если есть формальная спецификация?

  1. model checking vs. формальное доказательство (Isabelle и Coq).

  2. synthesis vs. refinement

  3. Cлучай Microsoft Iron Fleet

  4. D. Knuth, letter to Dr. P. van Emde Boas, April 1977:

ihaveonlyproved

Что почитать/посмотреть?

  1. Leslie Lamport. Specifying Systems: The TLA+ Language

  2. Hillel Wayne. Practical TLA+

  3. Jack Vanlightly. Heisenbug-Piter 2019. A systematic approach to building reliable distributed systems

Так нужна ли математика в тестировании?