| Spec# | |
|---|---|
| Класс языка | мультипарадигменный: структурный, императивный, объектно-ориентированный, событийно-ориентированный, функциональный, контрактный |
| Появился в | 2004 |
| Автор | Microsoft Research |
| Разработчик | Microsoft Research |
| Выпуск | 03.10.2011 (7 октября 2011) |
| Система типов | статическая, строгая, типобезопасная, номинативная |
| Испытал влияние | C#, Эйфель |
| Повлиял на | Sing# |
| Сайт | research.microsoft.com/s… |
Spec# — язык программирования с поддержкой особенностей языка спецификаций, расширяющих возможности языка программирования C# контрактным программированием, так, как это сделано в языке Эйфель, включая объектные инварианты, предусловия и постусловия. Как и ESC/Java, язык содержит инструмент статической проверки, основанный на доказательстве теорем, позволяющий статически проверять большинство таких инвариантов. Также он включает в себя множество других не столь значимых дополнений, как например, ненулевые ссылочные типы.
Microsoft Research разработала оба языка Spec# и C#. Spec# же послужил основой для создания языка Sing#, разработанный также Microsoft Research.