CTESK

В настоящее время в CTESK cуществует два типа покрытий:

1. Глобальные покрытия: информацию о покрытии сбрасывает пользователь, в отчетах отображаются в списке глобальных покрытий.
2. Локальные для спецификационных функций покрытия: информация о покрытии сбрасывается автоматически, в отчетах отображаются привязанными к спецификационным функциям.
   Необходимо реализовать третий вариант, когда информацию о покрытии сбрасывает пользователь, но в отчетах они отображаются привязанными к спецификационным функциям.

Проект синтаксиса: если к локальному покрытию добавлен модификатор post, такое покрытие автоматически трассироваться не должно. Область видимости его имени и элементов такая же, как и для обычных локальных покрытий: постусловие функции.

specification double sqrt_spec(double x) {
  pre { ... }
  coverage C { ... }
  post coverage D { ... }
  post { ... }
}