Transcript Software System Verification and Validation Laboratory Assignment 1

Verificare şi Validarea Sistemelor Soft
Temă Laborator 1
ESC/Java2
Extended Static Checker for Java
Dată primire laborator: Lab 1
Dată predare laborator: Lab 1 si Lab 2
Verificare şi Validarea Sistemelor Soft
• Software engineering problem: building/maintaining correct systems.
• How?
• Specification
• Tools
You don’t brake contract,
that’s illegal!
• Contract
• between caller (~user) and implementation (~provider).
• What the implementation can expect from the caller.
• What the caller can expect from the implementation.
Verificare şi Validarea Sistemelor Soft
Method contract
Postcondition
Precondition
Specifies “implementation’s responsibility”
Specifies “caller’s responsibility”
Constraints on the method’s return value and side effects.
•
Constraints on parameter values and target object’s state. •
Relation between initial and final state of the method.
•
Valid object’s states, in which a method can be called. •
Intuitively
Intuitively
•
Expression that must hold at the exit from the method.
•
Expression that must hold at the entry to the method.
Class contract
Invariant
•
Specifies caller’s responsibility at the entry to a method and implementation’s responsibility at the exit from a method.
•
Valid states of class instances (values of fields).
Intuitively
•
Expression that must hold at the entry and exit of each method in the class.
What is ESC/Java2?
http://secure.ucd.ie/products/opensource/ESCJava2/
• A programming tool that attempts to find common run-time errors in Java
programs by static analysis of the program text.
• ESC/Java versions are based around the Java Modeling Language (JML).
– JML follows the design by contract paradigm. It is a specification
language for Java programs, using Hoare style pre- and postconditions
and invariants. The specifications are added as Java annotation
comments to the Java program, which hence can be compiled with any
Java compiler.
– http://www.eecs.ucf.edu/~leavens/JML/
• 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 - installation
• See
– The txt file with information about installation.
– http://secure.ucd.ie/products/opensource/ESCJava2/
ESC/Java2 – by example
Demo 01: Fast exponentiation
Demo 02: MyArray
Demo 03: MySet
Verificare şi Validarea Sistemelor Soft
Temă Laborator 1
• ESC/Java2 - Extended Static Checker for Java
• Dată primire laborator: Lab 1
• Dată predare laborator: Lab 1 si Lab 2
• A se vedea fişierul TemaLab01_ESCJava2.pdf