Spec Sharp

Spec#

Класс языка:	мультипарадигменный: структурный, императивный, объектно-ориентированный, событийно-ориентированный, функциональный, контрактный
Появился в:	2004 г.
Автор(ы):	Microsoft Research
Последняя версия:	1.0.21125
Типизация данных:	статическая, строгая, типобезопасная, номинативная
Испытал влияние:	C#, Эйфель
Повлиял на:	Sing#

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

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

Пример

Данный пример демонстрирует две базовые структуры, используемые при добавлении контрактов ваш код. <source lang="csharp">

   static void Main(string![] args)
       requires args.Length > 0
   {
       foreach(string arg in args)
       {
           Console.WriteLine(arg);
       }
   }

</source>

• ! используется для создания ненулевого ссылочного типа, т.е. вы не сможете присвоить ему нулевое значение. Это отличается от нулевых типов, которые допускают присваивание им значений типа нуль.

• 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.

Смотри также

• Эйфель
• Singularity (операционная система)
• Sing#
• C#

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

• Веб-сайт Spec# от Microsoft Research
• Spec# на сайте Codeplex