Spec Sharp | это... Что такое Spec Sharp? (original) (raw)
Правильный заголовок этой статьи — Spec#. Он показан некорректно из-за технических ограничений.
Spec#
| Класс языка: | мультипарадигменный: структурный, императивный, объектно-ориентированный, событийно-ориентированный, функциональный, контрактный |
|---|---|
| Появился в: | 2004 |
| Автор(ы): | Microsoft Research |
| Релиз: | 1.0.21125 |
| Типизация данных: | статическая, строгая, типобезопасная, номинативная |
| Испытал влияние: | C#, Эйфель |
| Повлиял на: | Sing# |
| Сайт: | Spec# website |
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);
}
}- ! используется для создания ненулевого ссылочного типа, то есть вы не сможете присвоить ему нулевое значение. Это отличается от нулевых типов, которые допускают присваивание им значений типа нуль.
- 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
