Средства разработки приложений

         

Спецификации типов примера


Вопросы единственности типов, полноты типов (в смысле полноты системы аксиом), противоречивости типов (в смысле противоречивости системы аксиом), единственности реализации, оптимальности спецификации и реализаций, синтаксического сахара RSL и др. здесь не рассматриваются.

Попытаемся специфицировать типы описанных выше С++-реализаций Rectangle и Square на языке формальных спецификаций RSL в соответствии с методом, принятым в RDG. Дополнительный тип UReal (домен которого включает все положительные вещественные значения) вводится, чтобы функции были всюду определены, и не нужно было заниматься предусловиями.



Содержание раздела