Продолжается подписка на наши издания! Вы не забыли подписаться?

Обзор системы программирования Spec#

Автор: Mike Barnett K. Rustan M. Leino и Wolfram Schulte
Microsoft Research, Redmond, WA, USA
Опубликовано: 18.04.2007

Введение

Разработка ПО означает создание корректного и поддерживаемого программного обеспечения. Методики определения корректности программ получили развитие в конце 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#, ее дизайна, а также логических обоснований этого дизайна. Сейчас система находится в процессе разработки.

1 Язык

Язык Spec# – это расширение C#, объектно-ориентированного языка, созданного для платформы .NET. В C# имеется единичное наследование, что позволяет его классам реализовать множественные интерфейсы, объектные ссылки, динамически диспетчеризуемые методы, а также исключения – если говорить о наиболее существенных для этой статьи возможностях. Spec# вносит в C# поддержку типов, чтобы отличать объектные ссылки, не равные null, от объектных ссылок, возможно, равных null, спецификации методов (наподобие пред- и постусловий), порядок обработки исключений и поддержку ограничений для полей данных объектов. В этом разделе объясняются эти возможности и причины, обуславливающие их дизайн.

1.0 Не-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 типов недостаточно, программисты могут использовать контракты классов и методов, описанные ниже.

1.1 Контракты методов

Исключения

Предусловия

Постусловия

Исключительные постусловия

Frame-условия

Наследование спецификаций

1.2 Контракты классов

1.3 Другие подробности

Исключения в контрактах

Пользовательские атрибуты в спецификациях

Чистота

2 Архитектура системы

2.0 Проверки времени исполнения

2.1 Статическая проверка

2.2 Out-of-band спецификации и другое

3 Смежные работы

С упором на корректность и верификацию было разработано немало языков программирования. Это такие экспериментальные языки как 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 говорит, что поле указывает на принадлежащий кому-то объект.

4 Заключение

В основе системы программирования 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 и других за полезные комментарии при создании этой статьи.

Ссылки

  1. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
  2. Allen L. Ambler, Donald I. Good, James C. Browne, Wilhelm F. Burger, Richard M. Cohen, Charles G. Hoch, and Robert E. Wells. GYPSY: Alanguage for specification and implemen-tation of verifiable programs. SIGPLAN Notices, 12(3):1–10, March 1977. John Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003. With Praxis Critical Systems Limited.
  3. Mike Barnett, Robert DeLine, Manuel F?ahndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27–56, 2004.
  4. Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, and Arthur Watson. Serious specification for composing components. In Ivica Crnkovic, Heinz Schmidt, Judith Stafford, and Kurt Wallnau, editors, Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction, May 2003.
  5. Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes. Towards a tool environment for model-based testing with AsmL. In 3rd International Workshop on Formal Approaches to Testing of Software (FATES 2003), October 2003.
  6. Mike Barnett and David A. Naumann. Friends need a bit more: Maintaining invariants over shared state. In Dexter Kozen, editor, Mathematics of Program Construction, Lecture Notes in Computer Science, pages 54–84. Springer, July 2004.
  7. Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. 99.44% pure: Useful abstractions in specifications. In Erik Poll, editor, Proceedings of the ECOOP Workshop FTfJP 2004, Formal Techniques for Java-like Programs, pages 11–19, June 2004. University of Nijmegen, NIII report NIII-R0426.
  8. Mike Barnett and Wolfram Schulte. The ABCs of specification: AsmL, behavior, and com-ponents. Informatica, 25(4):517–526, November 2001.
  9. Mike Barnett and Wolfram Schulte. Runtime verification of .NET contracts. The Journal of Systems and Software, 65(3):199–208, 2003.
  10. Don Box. Essential .NET, Volume I: The Common Language Runtime. Addison-Wesley, 2002.
  11. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe pro-gramming: Preventing data races and deadlocks. In Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOP-SLA 2002, volume 37, number 11 in SIGPLAN Notices, pages 211–230. ACM, November 2002.
  12. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 2004. To appear.
  13. Roderick Chapman. Industrial experience with SPARK. Presented at SIGAda’00, November 2000. Available from http://www.praxis-cs.co.uk.
  14. Yoonsik Cheon. A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University, April 2003. Iowa State University, Department of Computer Science, Technical Report TR #03-09.
  15. Patrick Cousot and Rhadia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252. ACM, January 1977.
  16. Robert DeLine and Manuel F?ahndrich. Enforcing high-level protocols in low-level software. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 36, number 5 in SIGPLANNotices, pages 59–69. ACM, May 2001.
  17. Robert DeLine and Manuel F?ahndrich. Typestates for objects. In Martin Odersky, editor, ECOOP 2004 — Object-Oriented Programming, 18th European Conference, volume 3086 of Lecture Notes in Computer Science, pages 465–490. Springer, June 2004.
  18. 19
  19. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, July 2003.
  20. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December 1998.
  21. L. Peter Deutsch. An Interactive Program Verifier. PhD thesis, University of California, Berkeley, 1973.
  22. Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specifi-cation inheritance. In Proceedings 18th International Conference on Software Engineering, pages 258–267. IEEE, 1996.
  23. Manuel F?ahndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. In Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003, volume 38, num-ber 11 in SIGPLAN Notices, pages 302–312. ACM, November 2003.
  24. Robert Bruce Findler and Matthias Felleisen. Contract soundness for object-oriented lan-guages. In Proceedings of the 2001 ACM SIGPLAN Conference on Object-Oriented Pro-gramming Systems, Languages and Applications, OOPSLA 2001, volume 36, number 11 in SIGPLAN Notices, pages 1–15. ACM, November 2001.
  25. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), vol-ume 37, number 5 in SIGPLAN Notices, pages 234–245. ACM, May 2002.
  26. Robert W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposium in Applied Mathematics, pages 19–32. American Mathematical Society, 1967.
  27. Steven M. German. Automating proofs of the absence of common runtime errors. In Confer-ence Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 105–118, 1978.
  28. Donald I. Good, Ralph L. London, and W. W. Bledsoe. An interactive program verification system. In Proceedings of the international conference on Reliable software, pages 482–492. ACM, 1975.
  29. John B. Goodenough. Structured exception handling. In Conference Record of the Second ACM Symposium on Principles of Programming Languages, pages 204–224. ACM, January 1975.
  30. James Gosling, Bill Joy, and Guy Steele. The JavaTM Language Specification. Addison-Wesley, 1996.
  31. Wolfgang Grieskamp, Nikolai Tillmann, and Margus Veanes. Instrumenting scenarios in a model-driven development environment. Submitted manuscript, 2004.
  32. David Guaspari, Carla Marceau, and Wolfgang Polak. Formal verification of Ada programs. IEEE Transactions on Software Engineering, 16(9):1058–1075, September 1990.
  33. Yuri Gurevich, Benjamin Rossman, and Wolfram Schulte. Semantic essence of AsmL. The-oretical Computer Science, 2005. To appear.
  34. C. A. R. Hoare. An axiomatic approach to computer programming. Communications of the ACM, 12:576–580,583, 1969.
  35. C. A. R. Hoare. Monitors: an operating system structuring concept. Communications of the ACM, 17(10):549–557, October 1974.
  36. Bart Jacobs, K. Rustan M. Leino, and Wolfram Schulte. Verification of multithreaded object-oriented programs with invariants. In Proceedings of the workshop on Specification and Verification of Component-Based Systems, 2004. To appear.
  37. James C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385–394, July 1976. James Cornelius King. A Program Verifier. PhD thesis, Carnegie-Mellon University, Septem-ber 1969.
  38. Butler W. Lampson, James J. Horning, Ralph L. London, James G. Mitchell, and Gerald J. Popek. Report on the programming language Euclid. Technical Report CSL-81-12, Xerox PARC, October 1981. An earlier version of this report appeared as volume 12, number 2 in SIGPLAN Notices. ACM, February 1977.
  39. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175–188. Kluwer Academic Publishers, 1999.
  40. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: Abehavioral interface specification language for Java. Technical Report 98-06u, Iowa State University, Department of Computer Science, April 2003.
  41. K. Rustan M. Leino. Data groups: Specifying the modification of extended state. In Pro-ceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA ’98), volume 33, number 10 in SIGPLAN Notices, pages 144–153. ACM, October 1998.
  42. K. Rustan M. Leino. Extended static checking: Aten-year perspective. In Reinhard Wil-helm, editor, Informatics—10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 157–175. Springer, January 2001.
  43. K. Rustan M. Leino, Todd Millstein, and James B. Saxe. Generating error traces from verification-condition counterexamples. Science of Computer Programming, 2004. To ap-pear.
  44. K. Rustan M. Leino and Peter M?uller. Modular verification of global module invariants in object-oriented programs. Technical Report 459, ETH Z?urich, September 2004.
  45. K. Rustan M. Leino and Peter M?uller. Object invariants in dynamic contexts. In Martin Odersky, editor, ECOOP 2004 — Object-Oriented Programming, 18th European Confer-ence, volume 3086 of Lecture Notes in Computer Science, pages 491–516. Springer, June 2004.
  46. K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding. ACM Trans-actions on Programming Languages and Systems, 24(5):491–553, September 2002.
  47. K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. In Bart Jacobs, Gary T. Leavens, Peter M?uller, and Arnd Poetzsch-Heffter, ed-itors, Formal Techniques for Java Programs, Technical Report 251. Fernuniversit?at Hagen, May 1999.
  48. K. Rustan M. Leino and Wolfram Schulte. Exception safety for C#. In SEFM 2004—Second International Conference on Software Engineering and Formal Methods, pages 218–227. IEEE, September 2004.
  49. Barbara Liskov and John Guttag. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, 1986.
  50. D. C. Luckham. Programming with Specifications: An Introduction to Anna, a Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1990.
  51. 51. D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen,
  52. W. Polak, and W. L. Scherlis. Stanford Pascal Verifier user manual. Technical Report STAN-CS-79-731, Stanford University, 1979.
  53. Charles C. Mann. Why software is so bad. MIT Technology Review, July/August 2002.
  54. Steve McConnell. Code complete: A practical handbook of software construction. Microsoft Press, 1993.
  55. Bertrand Meyer. Object-oriented software construction. Series in Computer Science. Prentice-Hall International, 1988.
  56. Peter M?uller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002. PhD thesis, FernUni-versit?at Hagen.
  57. RTI Health, Social, and Economic Research. The economic impact of inadequate infras-tructure for software testing. RTI Project 7007.011, National Institute for Standards and Technology, May 2002.
  58. Mooly Sagiv, Thomas Reps, and Susan Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 167(1–2):131– 170, 1996.
  59. Alexandru S?alcianu and Martin Rinard. A combined pointer and purity analysis for Java programs. Technical Report MIT-CSAIL-TR-949, MIT, May 2004.
  60. Richard L. Sites. Proving that Computer Programs Terminate Cleanly. PhD thesis, Stanford University, May 1974. Technical Report STAN-CS-74-418.
  61. Joachim van den Berg and Bart Jacobs. The LOOP compiler for Java and JML. In Tiziana Margaria and Wang Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 2031 of Lecture Notes in Computer Science, pages 299–312. Springer, April 2001.
  62. Mickey Williams. Microsoft Visual C# .NET. Microsoft Press, 2002.
  63. Jeannette Marie Wing. A two-tiered approach to specifying programs. PhD thesis, MIT Department of Electrical Engineering and Computer Science, May 1983. MIT Laboratory for Computer Science TR-299.
  64. William A. Wulf, Ralph L. London, and Mary Shaw. An introduction to the construction and verification of Alphard programs. IEEE Transactions on Software Engineering, SE-2(4):253–265, December 1976.
........................
"С полным содержанием данной статьи можно ознакомиться в печатной версии журнала"

Любой из материалов, опубликованных на этом сервере, не может быть воспроизведен в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав.

Copyright © 1994-2016 ООО "К-Пресс"