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.
См. также Эйфель Singularity (операционная система) Sing# C#
Дополнительные источники Веб-сайт Spec# от Microsoft Research Spec# на сайте Codeplex
Категория:Семейство языков программирования C Sharp Категория:Языки программирования семейства Си Категория:Классовые языки программирования Категория:Языки формальных спецификаций Категория:Microsoft Research