1) Интересует тема <тестирование циклов> — в теории сказано, что цикл разворачивают в линейный код и прогоняют столько раз сколько нужно для выбранного критерия структурного тестирования (C0, C1, C2). Однако, как это выполнить на практике ???
2) Необходима информация по формальной верификации. Какие существуют основные концепции кроме аксиоматического метода (пропозиционная алгебра или тройки Хоара) и индуктивных утверждения Флойда? Существуют ли другие механизмы?
3) Кто нибудь пробовал строить формальные спецификации на основе языка OCL? Или данный язык ограничений не подходит для этих целей?!
4) Также интересна тема автоматизации процессов верификации и тестирования!
Приветсвуются обстоятельные и детальные ответы! (По тестированию к Маейрсу не отправлять конкретики по циклам там нет). Если етсь хорошие ресурсы, то киньте ссылки.
