r95 - 19 Jun 2007 - 22:08:31 - Andrei KlimovYou are here: TWiki >  Refaldevel Web > VerificationOO

Верификация программ на объектно-ориентированных языках

Информация о методах верификации программ на объектно-ориентированных языках, средствах описания моделей программ и функциональных требований.

The Java Modeling Language (JML)

Избранные статьи по JML

  • Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1-38, March 2006. HTML. PDF-файл для членов ACM здесь: http://doi.acm.org/10.1145/1127878.1127884.
    • Это толстая статья с кучей примеров, которые можно быстро просмотреть, чтобы понять, с чем едят JML. См. раздел 2.
    • Более подробный отчет Department of Computer Science, Iowa State University, TR #98-06-rev29, January 2006. PDF.

  • Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe 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, 7(3):212-232, June 2005. Preprint PDF.
    • Это краткая старая (2002) статья, описывающая состояние дел на тот момент.

  • Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006. Corrected PDF.
    • Вводятся понятия JML: assertions, pre- and postconditions, invariants, frame properties, datagroups, and ghost and model fields.

JML в лекциях

Демо и приложения JML

JML Tools

  • JMLEclipse is an Eclipse plug-in that allows the integration of JML into Eclipse's Java Developmnet Tools (JDT)

  • ESC/Java, the Extended Static Checker for Java
    • "The Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts to find common run-time errors in JML-annotated Java programs by static analysis of the program code and its formal annotations. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with specially formatted comments called pragmas."
    • ESC/Java2 Home Page
    • in Wikipedia.

Другие проекты и системы

  • Microsoft Research SLAM.

Методы

  • Symbolic Model Checking -- не близок ли к суперкомпиляции?

Конференции, семинары, учебные курсы с литературой

-- Andrei Klimov - 23-26 Mar 2007

Edit | WYSIWYG | Attach | Printable | Raw View | Backlinks: Web, All Webs | History: r95 < r94 < r93 < r92 < r91 | More topic actions
 
R+

This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback