Технология Клиент-Сервер 2006'4 |
|||||||
|
Разработка ПО означает создание корректного и поддерживаемого программного обеспечения. Методики определения корректности программ получили развитие в конце 1960-х (наиболее известны работы Floyd [25] и Hoare [33]). За следующее десятилетие было разработано несколько систем, помогающих автоматизировать доказательство корректности программ (см., например, [37, 27, 51]). Чтобы лучше всего влиять на процесс программирования, можно стремиться усовершенствовать главный инструмент программиста: язык программирования. Действительно, множество языков программирования разрабатывались именно с учетом обеспечения корректности через спецификации и проверки, как, например, экспериментальные языки Gypsy [1] и Euclid [38]. Другие языки, возможно, самый известный из них Eiffel [54], превращают встроенные спецификации в runtime-проверки, динамически проверяя корректность при каждом исполнении программы.
Несмотря на эти пророческие обоснования и многочисленные победы над техническими проблемами, текущие методики разработки ПО остаются дорогостоящими и подверженными ошибкам (сравните [56, 52]). Наиболее распространены неформальные спецификации, документация, написанная естественным языком и стандартизированные описания библиотечных интерфейсов (см., например, [61]). Однако многочисленные предположения программиста остаются не описанными, что усложняет поддержку программы, потому что неявные предположения легко нарушить. Кроме того, ничто не помогает удостовериться в том, что программа работает согласно предположениям программиста, и что программист случайно не пропустил некоторые предположения. Мы думаем, что ситуация с разработкой ПО улучшилась бы, если бы записывалось и воплощалось в жизнь больше предположений. На самом же деле этого не будет, пока не упростится запись таких спецификаций, дающая не только долгосрочные, но и непосредственные преимущества.
Система программирования Spec# - это новая попытка наиболее эффективно производить высококачественное ПО. Для широкого внедрения она должна предоставлять полную инфраструктуру, включая библиотеки, инструменты, поддержку дизайна, встроенные возможности редактирования, и, что наиболее важно, быть легкой в использовании для многих программистов. Поэтому в качестве подхода мы выбрали интеграцию с существующей промышленной платформой, .NET Framework. Система программирования Spec# базируется на языке программирования Spec#, расширении существующего объектно-ориентированного .NET-языка программирования C#. Расширение C# состоит в конструкциях спецификаций, наподобие пре- и постусловий, не-null типах и некоторых средствах для реализации высокоуровневых абстракций данных. Кроме того, программные конструкции C# обогащаются возможностью использования методологии программирования Spec#. Мы допускаем взаимодействие с существующим кодом и библиотеками .NET, но гарантируем корректность только до тех пор, пока исходный код написан на Spec#. Спецификации также становятся частью исполнения программы, при этом они динамически проверяются. Система программирования Spec# состоит не только из язука и компилятора, она включает также автоматический верификатор программ Boogie, статически проверяющий спецификации. Система Spec# полностью интегрирована со средой Microsoft Visual Studio.
Основные составляющие системы программирования Spec#:
В данной статье дается обзор системы программирования Spec#, ее дизайна, а также логических обоснований этого дизайна. Сейчас система находится в процессе разработки.
Язык Spec# – это расширение C#, объектно-ориентированного языка, созданного для платформы .NET. В C# имеется единичное наследование, что позволяет его классам реализовать множественные интерфейсы, объектные ссылки, динамически диспетчеризуемые методы, а также исключения – если говорить о наиболее существенных для этой статьи возможностях. Spec# вносит в C# поддержку типов, чтобы отличать объектные ссылки, не равные null, от объектных ссылок, возможно, равных null, спецификации методов (наподобие пред- и постусловий), порядок обработки исключений и поддержку ограничений для полей данных объектов. В этом разделе объясняются эти возможности и причины, обуславливающие их дизайн.
Многие ошибки в современных программах проявляются как ошибки разыменования ссылок на null. Отсюда следует важность языка программирования, обеспечивающего способность различать выражения, которые могут дать в результате вычисления null, и которые наверняка не могут (экспериментальное подтверждение см. в [24, 22]). Мы хотели бы избавиться от таких ошибок вообще.
Мы решили ввести в Spec# поддержку отслеживания и запрета ссылок на null, так как считаем, что простейший способ указания на то, что ссылка не может содержать null – указать эту информацию в описании типа. Обратная совместимость с C# диктует, что ссылочный тип Т должен означать обнуляемый тип в Spec#, и что соответствующий ненулевой тип должен получить новый синтаксис, в Spec# он обозначается как Т!.
Главная сложность в ненулевой системе типов возникает при обращении к ненулевым полям частично сконструированных объектов, как показано в следующем примере:
class Student : Person { Transcript! t; public Student(string name, EnrollmentInfo! ei) : base(name) { t = new Transcript(ei); } } |
Поскольку объявлено, что поле t имеет не-null тип, конструктор должен присвоить t не-null значение. Однако заметьте, что в этом примере присвоение значения t происходит после вызова конструктора базового класса (как и должно быть в C#). На протяжении этого вызова t по-прежнему равно null, хотя поле уже доступно (например, если конструктор базового класса выполняет динамически диспетчеризуемый вызов метода). Это нарушает гарантии типобезопасности не-null системы типов.
В Spec# эта проблема решается синтаксически, благодаря тому, что конструкторам разрешено назначать инициализаторы полей прежде, чем конструируемый объект становится доступным для программы. Чтобы исправить предыдущий пример, нужно написать:
class Student : Person { Transcript! t; public Student(string name, EnrollmentInfo! ei) :t(new Transcript(ei)), base(name) { } |
Этот синтаксис инициализации полей Spec# заимствует у C++, но важно то, что Spec#, в отличие от C++, вычисляет инициализаторы полей до вызова конструктора базового класса. Заметьте, что такое инициализирующее выражение может использовать параметры конструктора. Это полезная возможность, которую мы считаем жизненно важной для любого дизайна не-null типов. Spec# требует инициализаторов для любого не-null поля.
Spec# позволяет использовать не-null типы только для того чтобы указать, что поля, локальные переменные, формальные параметры и возвращаемые типы не равны null. Элементы массива не могут иметь не-null типы, что исключает проблемы с инициализацией элементов массива и с ковариантными массивами C#.
Чтобы облегчить использование не-null типов для программистов, переходящих с C#, Spec# предусматривает выведение неравенства null для локальных переменных. Для этого компилятор Spec# выполняет анализ потока данных.
Мы остановились на этой простой системе не-null типов по трем причинам. Во-первых, проблемы со ссылками на null характерны для ООП; предложение решения может быть привлекательным для очень многих программистов. Во-вторых, наше простое решение покрывает большинство полезных не-null паттернов программирования. В-третьих, в условиях, для которых выразительности системы не-null типов недостаточно, программисты могут использовать контракты классов и методов, описанные ниже.
С упором на корректность и верификацию было разработано немало языков программирования. Это такие экспериментальные языки как Gypsy [1], Alphard [63], Euclid [38] и CLU [49], предлагавшие различный уровень формализации. В Gypsy, который был первым языком, включающим спецификации как неотъемлемую часть языка программирования, интегрированные в исходной код спецификации были предназначены непосредственно для верификации программы с помощью интерактивного блока доказательства теорем. Alphard был создан вокруг методологии программирования для создания и проверки объектоподобных структур данных, но проверки выполнялись вручную. В Euclid спецификации, написанные с помощью булевых выражений языка, проверялись во время исполнения, с той мыслью, что более сложные спецификации, содержащиеся в комментариях, будут использоваться неким внешним верификатором. Методология программирования CLU включала спецификации, но они записывались только как стилизованные комментарии.
Тремя современными системами с контрактами, оказавшими непосредственное влияние на практику программирования, являются are Eiffel [54], SPARK [2] и B [0].
Eiffel [54] – это объектно-ориентированный язык, используемый уже почти 20 лет. Стандартная библиотека хорошо документирована с помощью контрактов, так что контракты непременно попадают в поле зрения программиста. Контракты задействуются динамически. Однако без методологии, включающей условия modifies и поддерживающей инварианты объектов в присутствии обратных вызовов, нельзя обеспечить модульную статическую верификацию.
SPARK [2] – это ограниченное подмножество Ада, лишенное многих динамических возможностей языка – ссылок, динамического выделения памяти и работы с иерархией классов, но достаточно большое, чтобы применяться во многих встраиваемых приложениях. Praxis Critical Systems использовала SPARK в нескольких промышленных программах, и их измерения показали, что строгость SPARK может быть эффективной по цене [13]. SPARK предлагает набор статических средств, от легковесной проверки исправности до полной верификации с интерактивным блоком доказательства теорем. Совместимость с существующим языком имела высокий приоритет при разработке SPARK, как и в случае Spec#, но их подход несколько отличается от нашего.
Исключив сложности Ada, SPARK, тем не менее, добился того, что любая SPARK-программа может быть скомпилирована любым стандартным компилятором Ada, сохраняя свое SPARK-значение (все спецификации SPARK размещаются в стилизованных комментариях Ada и не используются компилятором). Наша цель, переход разработчиков средней квалификации на более высоко интегрированный язык, не позволяет использовать подход SPARK, заключающийся в создании подмножества существующего языка. Вместо этого мы создали Spec# в виде расширения существующего языка, надеясь поддержать легкость и постепенность освоения его новых возможностей.
Подход В [0] использует иную методологию создания программ: начинает с полных спецификаций и поддерживает процесс пошагового уточнения спецификаций до превращения их в компилируемые программы. Результирующие программы по выразительности аналогичны программам на SPARK. Эта методология, с успехом использованная при создании тормозной системы для парижского метро, порождает только корректные программы. Однако квалификация, необходимая для выполнения процесса уточнения, делает кривую обучения этой системы очень крутой и становится барьером для многих программистов. Неочевидно также, как расширить эту систему до выразительных абстракций, принятых в современном объектно-ориентированном программировании.
Java Modeling Language (JML) [39, 40] – это нотация спецификаций для Java-программ. JML-спецификации, включающие богатую разновидность контрактов методов, в исходном коде Java записываются как стилизованные комментарии. Вокруг JML создан впечатляющий набор средств, включая инструменты для документирования, runtime-проверок, юнит-тестирования, легковесной проверки контрактов и верификации программ [12]. Spec# предоставляет более целенаправленную методологию, чем JML, который, например, должен еще перенять работу с инвариантами объектов при наличии обратных вызовов. Дизайн Spec# в некоторой степени менее ограничен, чем у JML, так как JML не пытается заменить нижележащий язык программирования (что, например, позволяет Spec# ввести инициализаторы полей и блоки expose).
Язык AsmL [32] создавался с теми же намерениями, что и Spec#: быть доступным, широко используемым языком спецификаций, рассчитанным на объекно-ориентированные .NET-системы. Однако AsmL ориентирован на поддержку разработки, основанной на модели, с ее средствами моделирования программ, генерацией тестовых случаев и исследованием состояния на метауровне [5]. Наш опыт использования AsmL для спецификаций интерфейсов [8], runtime-верификации [9] и в текущем проекте [4] оказал влияние на дизайн Spec#. Сопутствующий тестовый инструмент SpecExplorer [30], сейчас используемый в Microsoft, использует язык Spec# для основанного на модели тестирования с возможностью генерирования тесовых случаев, проверки моделей с явным состоянием и runtime-проверкой соответствия.
Язык спецификаций для Ada Anna [50] позволяет программистам записывать важные дизайн-решения. Спецификации компилируются в runtime-проверки.
Первые механические системы для проверки корректности программ были задуманы и созданы несколько десятилетий назад. В их число входят ранние, еще не полностью автоматические системы King [37, 36] и Deutsch [20], Gypsy [27], а также Stanford Pascal Verifier [51]. Более поздние верификаторы программ – Penelope (для Ada) [31] и LOOP (для Java и JML) [60], оба требуют интерактивного доказательства теорем.
Используя ранние попытки Sites [59] и German [26], Extended Static Checker for Modula-3 (ESC/Modula-3) [19] изменил правила игры, используя мощь автоматического средства доказательства теорем не для доказательства полной функциональной корректности программ, но для ограниченной цели поиска обычных ошибок. Продолжая эту традицию, ESC/Java [24] обернул эту технологию в более простой язык (подмножество JML), стараясь предоставить практичный высокоточный инструмент для программистов средней квалификации. Ключевым компонентом, позволяющим этим ESC-средствам выполнять полезные проверки, является готовность пропускать определенные ошибки, поскольку это может привести к упрощению языка спецификаций и к большим шансам на успешную работу автомата доказательства теорем (см. также [42]). Boogie пытается проверять программу полностью, не пропуская ошибок; его способности ограничиваются зависимостью от простоты спецификаций.
Spec# предоставляет ограниченную систему типов, поддерживающую не-null типы. Более полный вариант системы типов предлагался Fahndrich и Leino [22]. Их дизайн справляется со сложностями не-null полей, вводя дополнительные типы raw для частично сконструированных объектов.
Предлагались различные средства работы с абстракциями, помогающие определять условия modifies в современных объектно-ориентированных языках ([46, 55, 41]).
Наша методология для инвариантов объектов и условий modifies для размещения структур в куче полагается на владение объектами [3, 45, 6]. Похожие эффекты достигаются с помощью типов владения и других alias-confinement стратегий ([16, 11]). Наиболее ранний из встреченных нами примеров – Alphard [63], где модификатор unique говорит, что поле указывает на принадлежащий кому-то объект.
В основе системы программирования Spec# лежат методология программирования Spec#, язык и компилятор Spec#, и статический верификатор программ Boogie.
Методология впервые описывает, как работать с инвариантами и подклассами. Язык Spec# воплощает эту методологию: Spec# обогащает C# не-null типами, контрактами, проверяемыми исключениями, дополнениями (comprehensions) и квантификацией. Компилятор Spec# использует комбинацию техники статического анализа и runtime-проверок для обеспечения непротиворечивости языка. Верификатор пытается проверять соответствие программы и ее спецификаций.
Мы пытаемся сделать систему Spec# практически полезным инструментом программирования, позволяющим обычному программисту записывать и проверять свои предположения. Поэтому мы начинаем с известного языка программирования и используем метафору проверки типов для раскрытия новых возможностей нашей технологии статических проверок. Мы не предлагаем способа аксиоматизации новых математических теорий. Вместо этого наш дизайн сосредоточен на ограниченных, частично функциональных спецификациях, которые могут быть записаны с использованием булевых выражений языка и кванторов.
Мы разрабатывали Spec#, рассчитывая на увеличение выигрыша по мере использования программистами большего числа его возможностей. Даже без создания собственных спецификаций программисты получат немедленный выигрыш от того, что их Spec#-код проверяется на соответствие частично специфицированной Base Class Library.
Наш дизайн Spec# расчитан на последовательно выполняемые программы, но мы уже расширяем нашу методологию для поддержки параллельного программирования [35]. Кажется похожим на правду, что Spec# может пригодиться при создании безопасных приложений. Интересно было бы исследовать комбинацию нашей методологии с обходящим стек механизмом безопасности доступа к коду (CAS) в контексте существующих библиотек разграничения прав, аутентификации и криптографии.
Многие коллеги помогали сделать Spec# таким, каков он есть: Colin Campbell, Rob DeLine, Manuel F?ahndrich, Wolfgang Grieskamp, Nikolai Tillmann и Margus Veanes. Peter Muller и David Naumann внесли вклад в создание более совершенной версии методологии для инвариантов объектов. Rob и Manuel – участники проекта Boogie. Благодарим Jim Larus и Sriram Rajamani за поддержку и полезные обсуждения. Craig Schertz предоставил средство для извлечения контрактов из существующего кода. Большое спасибо Herman Venter, чей вклад в реализацию языка Spec# и среды разработки неоценим. Наконец, благодарим Gary Leavens, Peter Muller и других за полезные комментарии при создании этой статьи.
Copyright © 1994-2016 ООО "К-Пресс"