Transcript Folie 1 - Institut für Informatik

Formal Methods of
Systems Specification
Logical Specification of Hard- and Software
Prof. Dr. Holger Schlingloff
Institut für Informatik der Humboldt Universität
and
Fraunhofer Institut für Rechnerarchitektur und Softwaretechnik
1.7.2008
Assertion Languages
• OCL is an assertion language for UML
• Similar assertian languages have been defined for
various programming languages
 Java Modeling Language (JML) for Java
 Spec# for C#
 PSL for VHDL
• General idea
 static analysis: try to verify the assertions without running
the program
 dynamic supervision: use the assertions to influence the
execution of the program
H. Schlingloff, Logical Specification
1.7.2008
Slide 2
Example: JML
Reference: http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/
• using Hoare style pre- and postconditions and
invariants
• specifications are added as Java annotations
(comments) to the Java program
 can also be stored in separate specification files
//@ <JML specification>
/*@ <JML specification> @*/
H. Schlingloff, Logical Specification
1.7.2008
Slide 3
JML Syntax
• assert
 Defines a JML assertion
• requires
 Defines a precondition on the method that follows
• ensures
 Defines a postcondition on the method that follows
• invariant
 Defines an invariant property of the class
• signals
 Defines a condition on when a given exception can be thrown by the
method that follows
• assignable
 Defines which fields are allowed to be assigned to by the method that
follows
H. Schlingloff, Logical Specification
1.7.2008
Slide 4
JML expressions
• Boolean Java expressions
• \result
 identifier for the return value of the method that follows
• \old(<name>)
 modifier to refer to the value of variable <name> at the
time of entry into a method (OCL @pre!)
• \forall, \exists
 universal and existential quantifier (for arrays etc.)
 range of quantification limited!
• a ==> b, a<==>b
 logical implications
H. Schlingloff, Logical Specification
1.7.2008
Slide 5
Example
public class Account {
public static final int MAX_BALANCE = 1000;
private int balance;
private boolean isLocked = false;
//@ invariant balance >= 0 && balance <= MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == 0;
public Account() { }
//@ requires amount > 0;
//@ ensures balance = \old(balance) + amount;
public void deposit(int amount) { … }
//@ ensures isLocked == true;
public void lockAccount() { this.isLocked = true; }
H. Schlingloff, Logical Specification
}
1.7.2008
Slide 6
Dynamic Analysis
• Generate extra code from annotations to
check violations




assert: check at the given statement
requires: check before entering the method
ensures: check at the end of the method
invariant: check after each statement
- obviously, only when statement might affect expression
• Use assertions to generate JUnit test cases
 set preconditions, get postconditions
H. Schlingloff, Logical Specification
1.7.2008
Slide 7
Static Analysis Tools
• Abstract interpretation tries to calculate
possible values of variables
 sound approximation to the possible ranges
 e.g., i  [-maxint..16], [17..21], [22..maxint]
i += 1  i  [-maxint..17], [18..22], [23..maxint]
• Formally, an abstraction function is a mapping
from a (large) concrete domain into a (small)
abstract domain; e.g., int  {neg, zero, pos}
 operations on concrete objects are replaced by
operations on abstract objects
H. Schlingloff, Logical Specification
1.7.2008
Slide 8
JML Screenshot
H. Schlingloff, Logical Specification
www-sop.inria.fr/.../bcwp/img/jmlCompile.jpeg
1.7.2008
Slide 9
Spec# and Spec Explorer
Microsoft‘s Road to Specification
• Evolving algebras (Egon Börger et al., 1990‘s)
 „Philosophical“ background
• ASMs and the ASML (Yuri Gurevich et al.)
 Theoretical background
• Spec# (Wolfram Schulte et al.)
 Interactive program verification
• Spec Explorer (Wolfgang Grieskamp et al.)
 Support for model-based testing
H. Schlingloff, Logical Specification
1.7.2008
Slide 10
Spec# Overview
http://www.cs.nuim.ie/~rosemary/ETAPS-SpecSharp-Tutorial.pdf
• Aiming at program verification
• Based on C# (which in turn is based on C++ and Java)
• Spec# is an extension of C# by non-null types, method contracts, object
invariants, and checked exceptions
 can be seen as a programming language of its own
• Tool support
 compiler
-
statically enforces non-null types
emits run-time checks for method contracts and invariants
records the contracts as metadata for consumption by downstream tools
 static program verifier „Boogie“
-
generates logical verification conditions from a Spec# program
uses automatic theorem prover
analyzes the verification conditions to prove the correctness of the
program or find errors in it
H. Schlingloff, Logical Specification
1.7.2008
Slide 11
Use of Spec#
• Write each class containing methods and their
specification together in a Spec# source file
 Invariants that constrain the data fields of objects
may also be included
• Run the verifier (either from IDE or command
line)
 push button, wait (maybe long), get a list of
compilation/verification error messages
 Interaction with the verifier is done by modifying
the source file
H. Schlingloff, Logical Specification
1.7.2008
Slide 12
Screenshot
Precondition not
satisfied
Wrong input
Log messages for
programmer
• Freely available, needs MSVS .Net
H. Schlingloff, Logical Specification
1.7.2008
Slide 13
Example
// non-null argument
assume: not checked but taken as granted
assert: statically or dynamically validated
H. Schlingloff, Logical Specification
1.7.2008
Slide 14
Swap Example
• How can the proof be performed?
H. Schlingloff, Logical Specification
1.7.2008
Slide 15
Spec# Verification
• focus on automation of verification rather than full functional
correctness of specifications
 No verification of liveness (termination or other temporal eventuality
properties)
 No arithmetic overflow checks (yet)
• Active research on extensions (e.g. comprehensions)
H. Schlingloff, Logical Specification
1.7.2008
Slide 16
Quantifiers
• Quantification on finite domains!
 Verification can be expensive (search all values)
H. Schlingloff, Logical Specification
1.7.2008
Slide 17
Loop Invariants
• Can help the solver to reach its goal !
H. Schlingloff, Logical Specification
1.7.2008
Slide 18
Loop Invariants
• Can help the solver to reach its goal !
H. Schlingloff, Logical Specification
1.7.2008
Slide 19
H. Schlingloff, Logical Specification
1.7.2008
Slide 20
BoogiePL
• Simple procedural language for .Net
if (condition) S else T
Spec#:
BoogiePL:
Then
branch
assume condition;
S
H. Schlingloff, Logical Specification
assume ! condition;
T
1.7.2008
Else
branch
Slide 21
BoogiePL syntax
H. Schlingloff, Logical Specification
1.7.2008
Slide 22
H. Schlingloff, Logical Specification
1.7.2008
Slide 23
BoogiePL Verifier
• Based on HP‘s „Simplify“ theorem prover
 http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf
 first-order theorem prover (satisfiability)
 includes complete decision procedures for the theory of
equality and for linear rational arithmetic
 heuristics for linear integer arithmetic
 propositional connectives are solved by backtracking
 handling of quantifiers by pattern-driven instantiation
(incomplete)
• Translation from Boogie PL to Simplify
 weakest precondition of each statement
 each statement and each procedure gives rise to one
verification condition
H. Schlingloff, Logical Specification
1.7.2008
Slide 24