Русская Википедия:Spec Sharp

Материал из Онлайн справочника
Версия от 15:17, 17 июля 2023; EducationBot (обсуждение | вклад) (Новая страница: «{{Русская Википедия/Панель перехода}} {{title|Spec#}} {{Карточка языка программирования | name =Spec# | logo = | paradigm = мультипарадигменный: структурный, императивный, Объектно-ориентированное програм...»)
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигацииПерейти к поиску

Шаблон:Title Шаблон:Карточка языка программирования Spec# — язык программирования с поддержкой особенностей языка спецификаций, расширяющих возможности языка программирования C# контрактным программированием, так, как это сделано в языке Эйфель, включая объектные инварианты, предусловия и постусловия. Как и ESC/Java, язык содержит инструмент статической проверки, основанный на доказательстве теорем, позволяющий статически проверять большинство таких инвариантов. Также он включает в себя множество других не столь значимых дополнений, как например, ненулевые ссылочные типы.

Microsoft Research разработала оба языка Spec# и C#. Spec# же послужил основой для создания языка Sing#, разработанный также Microsoft Research.

Пример

Данный пример демонстрирует две базовые структуры, используемые при добавлении контрактов в ваш код.

    static void Main(string![] args)
        requires args.Length > 0
    {
        foreach(string arg in args)
        {
            Console.WriteLine(arg);
        }
    }
  • ! используется для создания ненулевого ссылочного типа, то есть вы не сможете присвоить ему нулевое значение. Это отличается от нулевых типов, которые допускают присваивание им значений типа null.
  • requires («требует») означает условие, выполнимое в данном коде. В этом случае длина args не должна быть равной нулю или меньше.

Источники

  • Barnett, M., K. R. M. Leino, W. Schulte, «The Spec# Programming System: An Overview.» Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), Marseilles. Springer Science+Business Media, 2004.

См. также

Дополнительные источники

Шаблон:Compu-lang-stub Шаблон:DotNET Шаблон:Microsoft Research