 | Эта статья включает в себя список литературы , связанной литературы или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( Август 2016 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
| Парадигма | мультипарадигма : структурированная , императивная , объектно-ориентированная , событийно-ориентированная , функциональная , контрактная |
|---|---|
| Разработано | Microsoft Research |
| Разработчик | Microsoft Research |
| Впервые появился | 2004 |
| Стабильный выпуск | SpecSharp 2011-10-03 / 7 октября 2011 г . |
| Печатная дисциплина | статический , сильный , безопасный , именительный падеж |
| Лицензия | Лицензионное соглашение с общим исходным кодом Microsoft Research (MSR-SSLA) |
| Веб-сайт | исследование |
| Под влиянием | |
| C # , Эйфелева | |
| Под влиянием | |
| Петь# | |
Spec # - это язык программирования с функциями языка спецификаций, который расширяет возможности языка программирования C # с помощью контрактов , подобных Eiffel , включая объектные инварианты , предварительные и постусловия. Как и ESC / Java , он включает в себя инструмент статической проверки, основанный на программе доказательства теорем, которая может статически проверять многие из этих инвариантов. Он также включает множество других второстепенных расширений языка, таких как ненулевые ссылочные типы.
Код контракты API в .NET Framework 4.0 эволюционировала с Spec #.
Microsoft Research разработала как Spec #, так и C # ; в свою очередь, Spec # служит основой языка программирования Sing # , который также был разработан Microsoft Research.
Особенности [ править ]
- См. Также: Spec # в синтаксисе C Sharp .
Spec # расширяет базовый язык программирования C # такими функциями, как:
- Типы, не допускающие значения NULL
- Структуры для контракта кода, такие как предусловия и постусловия .
- Проверены исключения, аналогичные таковым в Java .
- Удобный синтаксис
Пример [ править ]
В этом примере показаны две основные структуры, которые используются при добавлении контрактов в ваш код ( попробуйте Spec # в своем браузере ).
static int Main ( string ! [] args ) требует аргументов . Длина > 0 ; обеспечивает return == 0 ; { foreach ( строка arg в args ) { Console . WriteLine ( аргумент ); } return 0 ; }- ! используется, чтобы сделать ссылочный тип не допускающим значения NULL, например, вы не можете установить значение NULL. В этом отличие от типов, допускающих значение NULL, которые позволяют задавать типы значений как NULL .
- requires указывает на предварительное условие, которое должно соблюдаться в коде. В этом случае длина аргументов не может быть равна нулю или меньше.
- гарантирует указывает постусловие, которое должно соблюдаться в коде.
Спой # [ править ]
Sing # - это расширенный набор Spec #. Microsoft Research разработала Spec #, а затем расширила его до Sing #, чтобы разработать операционную систему Singularity . Sing # расширяет возможности Spec # за счет поддержки каналов и конструкций низкоуровневого языка программирования , которые необходимы для реализации системного программного обеспечения . Sing # безопасен по типу. Семантика примитивов передачи сообщений в Sing # определяется формальными и письменными контрактами. [ необходима цитата ]
Источники [ править ]
- Барнетт, М., KRM Leino, W. Schulte, "Система программирования Spec #: Обзор". Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS) , Marseilles. Springer-Verlag , 2004.
См. Также [ править ]
- Эйфелева
- Сингулярность
- C #
Внешние ссылки [ править ]
- Веб-сайт Spec # от Microsoft Research
- Номер спецификации в Codeplex
- Онлайн-спецификация # на RiSE4fun
