Привет! Представляю вашему вниманию перевод статьи «FORMALLY SPECIFYING UIS» автора Hillel Wayne.
От автора
Относительно недавно я наткнулся на статью про Инженерные методы в разработке ПО, где vasil-sd рассказал про формальную валидацию спецификаций к создаваемым программным продуктам. В качестве инструментария был использован Alloy. Одним из основных лейтмотивов в комментариях был — разобрать статью в контексте какого-нибудь современного веб проекта, потому что дорогодолгосложно использовать формальные методы там, где все делают быстродешево. Так как автор ссылался на блог Hillel Wayne, где такие примеры были, я решил перевести что-то из его статей в качестве дополнения к основному тексту vasil-sd
Предупреждение:
- Все, что автор называет finite-state machine, я буду называть конечным автоматом или моделью конечного автомата.
- Часть терминологии я почерпнул из статьи, ранее мною упомянутой, об инженерном подходе к разработке. Тем не менее, тема для меня относительно новая, потому обоих авторов(как зарубежного, так и не очень) мог понять не так — не ругайтесь.