Мультивселенная C# – сингулярность языка программирования
Перевод на английский – Medium. Перевод на украинский – DOU.
Свое знакомство c .NET и C# я начал где-то в 2007 году. Я тогда учился на 4 курсе и на тот момент у меня уже был опыт работы с такими языками программирования как C++ и Delphi. Более того, у меня был даже коммерческий продукт, написанный на Visual C++ и вполне неплохо работавший. Но уже тогда мне было тесно в тех рамках, которые задавали как Delphi, так и C++, я начал искать альтернативы. Я по чуть-чуть поработал с разными языками и технологиями, а когда добрался до C#, то сразу же понял – вот инструмент, который на сто процентов отвечает моим запросам и с которым комфортно и удобно работать. С тех пор я активно слежу за всем, что происходит с платформой .NET и языком C#. Во всяком случае мне так казалось до недавнего времени, пока ко мне не попали на глаза кое-какие публикации, из которых я узнал, что помимо привычного и знакомого нам C#, существует еще несколько «параллельных реальностей», где все вроде бы, как и здесь, но немного иначе. Вот с этими альтернативными реальностями я и предлагаю познакомиться немного ближе.
Для начала нам придется вернуться во времени где-то так лет на двадцать. Именно в 2003 [1]году, в недрах Microsoft Research (это исследовательское подразделение корпорации Microsoft, практически секретная лаборатория) была начата работа над проектом Singularity – высоконадёжной операционной системой, в которой микроядро, драйвера устройств и приложения написаны на управляемом коде.
В своей статье «Singularity: Rethinking the Software Stack» сотрудники Microsoft ResearchДжеймс Ларус и Гален Хант пишут о Singularity так [2]: «Работая над проектом мы создали новую операционную систему, новый язык программирования и новые инструменты проверки программного обеспечения. Операционная система Singularity включает новую программную архитектуру, основанную на программной изоляции процессов. Наш язык программирования Sing# является расширением C#, обеспечивающим поддержку коммуникационных примитивов ОС, а также поддержку системного программирования и факторизации кода.»
История создания операционной системы Singularity сама по себе невероятно интересная и заслуживает отдельной статьи. Но в данном случае меня заинтересовала фраза «наш язык программирования Sing#». Я никогда прежде не слышал о таком языке программирования и мне стало интересно узнать о нем побольше. Статья в Википедии [3] об этом языке оказалась очень короткой и была представлена всего в двух языковых версиях – русской и немецкой. Но несмотря на малый объем информации там обнаружилось еще кое-что интересное – в карточке описания языка указывалось, что Sing# испытал влияние еще одного, неизвестного мне доселе другого языка – Spec# [3]. Получается, что у нас уже есть целых два ответвления от C#.
Поскольку Spec# является основой для Sing#, то и искать более детальную информацию я начал с него. Сама команда Microsoft Research так характеризует этот язык [4]: «Spec# — это формальный язык для контрактов API, который расширяет C# конструкциями для ненулевых типов, предусловий, постусловий и инвариантов объектов.»
Про Sing#, согласно публикации «An Overview of the Singularity Project» говорится следующее [5]: «Sing# является расширением языка Spec#, разработанного в Microsoft Research. Sing# расширяет этот язык поддержкой каналов и низкоуровневых конструкций, необходимых для системного кода.»
Напомню, что речь идет разработках, которые велись с примерно 2003 года по 2015 год. То есть времени с того момента прошло довольно много, но концепции, заложенные в те языки программирования и сейчас выглядят весьма прогрессивными. Стоит отдать должное сумрачным гениям из Microsoft Research – они мало того, что не засекретили информацию об этих разработках, он даже собрали и опубликовали большое количество материалов на сайте проекта. Изучать статьи и публикации можно достаточно долго – я пока смог прочитать (а скорее даже просмотреть), лишь малую часть из представленных материалов. В процессе ознакомления со статьями мне стало интересно, а оказали ли языки из «параллельных реальностей» влияние на C# и .NET, какими мы их знаем сегодня?
Проведя небольшое исследование, я обнаружил, что влияние это безусловно есть. Несмотря на то, что и Sing# и Spec# не получили дальнейшего развития, успешные идеи действительно были впоследствии внедрены в C# – какие-то раньше, какие-то позже.
На сегодня мы точно можем сделать вывод, что ряд концепций был изначально реализован в процессе работы над экспериментальными инкарнациями языка:
Сейчас я предлагаю внимательнее посмотреть на то, как каждая из упомянутых выше концепций была представлена изначально и какую реализацию получила сейчас.
Code Contracts
Проект Code Contracts является ответвлением Spec# и предоставляет способ определения предусловий, постусловий и инвариантов объектов в коде [6]:
- Предусловия являются требованиями, которые должны быть выполнены при входе в метод или свойство.
- Постусловия описывают ожидания на момент завершения работы кода метода или свойства.
- Инварианты объекта описывают ожидаемое состояние класса, находящегося в нормальном состоянии.
Преимущества, которые предлагает использование Code Contracts [8]:
- Улучшенное тестирование: проверка контрактов на этапах как компиляции, так и выполнения.
- Инструменты автоматического тестирования: Code Contracts могут использоваться для генерации более осмысленных тестов, отфильтровывая аргументы теста, которые не удовлетворяют предусловиям.
- Статическая проверка: статический анализатор может определить нарушения контрактов без запуска программы. Он проверяет неявные контракты, такие как нулевые ссылки и границы массива, и явные контракты.
- Справочная документация: генератор документации дополняет существующие файлы документации информацией о контрактах.
Отмечу, что на сегодня Code Contracts уже не поддерживаются в .NET 5 и более новых версиях платформы, теперь вместо них предлагается обратить внимание на использование nullable referencetypes [8].
Если мы посмотрим на спецификацию Spec#, то увидим такое определение [9]: «Одним из основных элементов спецификации в Spec# является метод. Каждый метод может включать предусловие, которое описывает условия, при которых вызов метода разрешен, и постусловие, которое описывает условия, при которых возврат метода разрешен. Следовательно, реализация метода может предполагать, что предусловие соблюдается при входе, и вызывающий метод может предполагать, что постусловие соблюдается при возврате. Это соглашение между вызывающими метод и реализацией часто называется контрактом метода.»
Таким образом, мы можем сделать вывод, что концепция контрактов является одной из основополагающих для Spec#и нашла свое органическое продолжение в реализации code contracts.
Non-null reference types
В восьмой версии языка C# Microsoft ввела понятие non-nullable references, которое позволяют разработчику гарантировать, что ссылочный тип не может быть нулевым. Это достигается за счет проверок на этапе компиляции, что в свою очередь позволяет создавать программы более простыми и надежными.
Концепция non-null reference types также уходит своими корнями в Spec#, как и концепция CodeContracts. В Spec# объявление non-null reference выглядело так:
Стоит отметить, что Энтони Хоар, один из создателей языка программирования ALGOL W, заявляет, что концепцию null reference предложил именно он. И сегодня он считает, что это была «ошибка на миллиард долларов» [10]:
«Я называю это своей ошибкой на миллиард долларов. Это было изобретение нулевой ссылки в 1965 году. В то время я разрабатывал первую комплексную систему типов для ссылок в объектно-ориентированном языке (ALGOL W). Моя цель состояла в том, чтобы гарантировать, что любое использование ссылок должно быть абсолютно безопасным, с автоматической проверкой компилятором. Но я не мог устоять перед искушением указать нулевую ссылку просто потому, что это было так легко реализовать. Это привело к бесчисленным ошибкам, уязвимостям и системным сбоям, которые, вероятно, причинили миллиарды долларов ущерба за последние сорок лет.»
Думаю, что в этом с Тони согласятся все разработчики, кому хоть раз доводилось сталкиваться с null pointer exception.
«Чтобы сделать использование non-null типов еще более удобным для программистов, переходящих на Spec# с C#, Spec# предписывает вывод non-nullity для локальных переменных. Этот вывод выполняется в виде анализа потока данных компилятором Spec#.» [11]
readonly / pure methods
В девятой версии языка C# была реализована возможность объявления структур только для чтения – readonly struct [12]. Структура, объявленная с ключевым словом readonly гарантирует, что ни один из ее элементов не изменит состояние структуры. При этом ключевое слово readonly может применяться как ко всей структуре, так и к ее отдельным полям, или методам.
Схожее поведение было реализовано в Sing# через атрибут Pure: метод (функция принадлежащая классу) называется чистым и объявляется как таковой атрибутом Pure в том случае, если он возвращает значение без изменения состояния. Чистые методы не должны иметь побочных эффектов [13]:
Тут я бы обратил внимание еще не один интересный момент: функциональное программирование иногда рассматривается как синоним чистого функционального программирования, подмножества функционального программирования, которое рассматривает все функции как чистые функции [14]. В последнее время можно заметить, как активно концепции функционального программирования входят и довольно органично встраиваются в привычные нам объектно-ориентированные языки.
Выводы
Вполне допускаю, что список обнаруженных мною примеров влияния Spec# и Sing# на C# далеко не полон и ознакомившись с материалами более внимательно, чем я, вы найдете и друге схожие концепции на генетическом уровне языков программирования. А чтобы заниматься исследованиями вам было проще, я прилагаю список полезных материалов:
· Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs
· The Spec# Programming System: An Overview
· Singularity: Rethinking the Software Stack
· An Overview of the Singularity Project
· Language Support for Fast and Reliable Message-based Communication in Singularity OS
· The Spec# Programming System: Challenges and Directions
Bibliography
[1]Microsoft, "Singularity," [Online]. Available: https://www.microsoft.com/en-us/research/project/singularity/.
[2]H. С. Galen and R. L. James, "Singularity: Rethinking the Software Stack," [Online]. Available: https://courses.cs.washington.edu/courses/cse551/15sp/papers/singularity-osr07.pdf.
[3]Wikipedia, "Spec#," [Online]. Available: https://ru.wikipedia.org/wiki/Spec_Sharp.
[4]Microsoft, "Spec#," [Online]. Available: https://www.microsoft.com/en-us/research/project/spec/.
[5]Microsoft Research, "An Overview of the Singularity Project," [Online]. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/10/tr-2005-135.pdf.
[6]M. Lapierre, "Introducing Advanced Code Contracts with the Entity Framework and Pex," [Online]. Available: https://www.codemag.com/Article/1001101/Introducing-Advanced-Code-Contracts-with-the-Entity-Framework-and-Pex.
[7]"Code contracts (.NET Framework)," [Online]. Available: https://github.com/dotnet/docs/blob/main/docs/framework/debug-trace-profile/code-contracts.md.
[8]"Code contracts (.NET Framework)," [Online]. Available: https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts.
[9]K. R. M. L. and P. Müller, "Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs," [Online]. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml189.pdf.
[10]"Null pointer," [Online]. Available: https://en.wikipedia.org/wiki/Null_pointer#History.
[11]"The Spec# Programming System: An Overvie," [Online]. Available: https://www.cs.cornell.edu/courses/cs711/2005fa/papers/bls-cassis04.pdf.
[12]Microsoft, "Structure types (C# reference)," [Online]. Available: https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/builtin-types/struct#readonly-struct.
[13]"Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs," [Online]. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml189.pdf.
[14]Wikipedia, "Functional programming," [Online]. Available: https://en.wikipedia.org/wiki/Functional_programming.