Transcript END - 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
3.6.2008
Question from last week
Q.: Is there anything which can not be specified with
Z?
 anything = a function from Nat to Nat
A.: The number of possible Z specifications is at most
countable, while there are uncountably many such
functions
 More general, the number of possible specifications in any
well-defined specification formalism is at most countable
 yet, it is hard to find a „natural“ function which is not
specifiable, since the formalism is designed especially to
formulate all „natural“ functions…
H. Schlingloff, Logical Specification
3.6.2008
Slide 2
repetition: Z
• Basic building blocks: Z schemes
 declarations (signature)
 predicates (formulas constraining variable values)
•
•
•
•
High expressiveness by set theory and logic
Possibility of under-specification in Z
Modularity (but no object orientation)
Well-suited for program verification
• Not well-suited for refinement (transformational
program development) and/or test generation
H. Schlingloff, Logical Specification
3.6.2008
Slide 3
B-method
• Tries to overcome this shortcoming
• Aiming at program development and proof
 refinement, implementation, code generation
 generalized substitution
• The B method was developed by J.-R. Abrial (co•
•
author of Z) as an extension of Z
Several commercial and university tools
Various case-studies in safety-critical systems
H. Schlingloff, Logical Specification
3.6.2008
Slide 4
Substitution in Predicate Logic
• Needs distinction between free and bound variable
occurrences
 occurrences of x in t(… x…) and p(… x …) are free
 every occurrence of x in  is bound in x 
 a variables can have free and bound occurrences in a
formula
• [x:=t] is the formula derived from  by replacing
every free occurrence of x with term t
 substitution may not create new bound occurrences of
variables; e.g. ((x )[x:=t])
x y p(x,y)  (y p(x,y))[x:=y]
x y p(x,y)  y p(y,y)
 inductive definition of „t is free for y in “
H. Schlingloff, Logical Specification
3.6.2008
Slide 5
Substitutions in B
• Written in prefix notation
 [x:=t] instead of [x:=t]
 [x:=2](x5) is (25), a true statement
• Substitution as assignment („predicate transformer“)
 read as: if x is assigned 2, then x is less or equal to 5
 [] can be interpreted as “ establishes ”
 Derived from E.Dijkstra‘s wp- (weakest precondition-)
calculus
• Program specification
 admissible starting states specified by formula ,
desired final states specified by formula 
 a program is a generalized substitution  such that
([])
H. Schlingloff, Logical Specification
3.6.2008
Slide 6
B
• Based on abstract machines
 don‘t confuse with abstract state machines (ASM)
• Predicates define properties of abstract machines (states of
interest)
 a state is a valuation of variables
• Substitutions define value changes, allow to transform
predicates
 generalized substitutions can be seen as operations on states
• Invariants are properties which hold in all states
 similar to Z formulas
 often used to define type constraints
• Initialization is by a special substitution
• Refinements define transformations between abstract
machines
H. Schlingloff, Logical Specification
3.6.2008
Slide 7
Global View
Reference: Most of the following material is taken from Moreira, Deharbe, Software Engineering with the B method; 8th Braz. Sym. on FM,
http://www.consiste.dimap.ufrn.br/~david/files/sbmf05-tutorialb.pdf
H. Schlingloff, Logical Specification
3.6.2008
Slide 8
Basic Structure of an Abstract Machine
MACHINE Name (Parameters)
VARIABLES list of variables
INVARIANT
invariant predicate
INITIALISATION
initialization substitution
OPERATIONS
outputs  name(inputs) ≙ substitution
END
H. Schlingloff, Logical Specification
3.6.2008
Slide 9
Example
MACHINE BirthdayAgenda (NAME, DATE)
VARIABLES known, birthday
INVARIANT known  NAME  birthday  known  DATE
INITIALISATION known, birthday := , 
OPERATIONS
Register (n, d) ≙
PRE
n  NAME  d  DATE  n  known
THEN known := known  {n} ||
birthday := birthday  {n ↦ d}
END
d  FindBirthday (n) ≙
PRE
n  NAME  n  known
THEN d := birthday(n)
END;
END
H. Schlingloff, Logical Specification
a  FindParty (d) ≙
PRE d  DATE
THEN a := birthday-1 (d)
END
3.6.2008
Slide 10
Verification of a Specification
• The initialization shall establish the invariant
 The machine shall initiate in a valid state
 Proof obligation: [], where  is the initialization
substitution, and  is the invariant predicate
• The operations shall preserve the invariant
 The operations of the machine shall not take it into an
invalid state, assuming that their pre-conditions are
respected
 Proof obligation: (    [] ), where
-  is the invariant predicate,
-  is the pre-condition of the operation, and
-  is the substitution of the operation
H. Schlingloff, Logical Specification
3.6.2008
Slide 11
Example
H. Schlingloff, Logical Specification
3.6.2008
Slide 12
Generalized Substitutions
•
•
•
•
•
•
•
•
•
•
[1;2] is [2][1] 
[1||2] is [1][2]  (disjoint sets of variables)
[x,y:=s,t] is [tmp:=t][x:=s][y:=tmp]
[IF  THEN 1 ELSE 2 END] is
(([1])  (¬[2]))
[SELECT 1 THEN 1 WHEN 2 THEN 2 END] is
((1  [1])  (2  [2]))
[SKIP] is 
[ANY x WHERE  THEN  END] is x ( [])
[CHOICE 1 OR 2 END] is ([1]   [2] )
[PRE  THEN  END] is (  [])
…
H. Schlingloff, Logical Specification
3.6.2008
Slide 13
Modularization
• An abstract B machine can
 USE
 SEE
 INCLUDE
 PROMOTE
 EXTEND
other abstract machines
• That way, it is possible to build complex libraries of
•
abstract machines
Rich libraries are available for most basic types
H. Schlingloff, Logical Specification
3.6.2008
Slide 14