Report

The B Method by Péter Györök Contents • • • • Metadata The B language The Prover Demo People behind it • Developed by Jean-Raymond Abrial – Other people: G. Laffite, F. Mejia, I. McNeal • Currently big companies and various universities maintain it • ClearSy, Oxford University (Programming Research Group) • Subsidised projects History, origin, versions • Predecessor: Z-notation (also by Abrial) • Newest incarnation: Event-B • Tools: Atelier B, B4free, B-toolkit Primary application domain • Software engineering – Specification – Design – Proof – Code generation • Safety-critical systems • Big companies that use it: Siemens, Alstom, Systerel… Success stories • METEOR project – Paris Metro Line 14 – (Hungarian relevance?) • Ariane 5 (rocket) System overview • B notation based on group theory and first order logic • The method is heavily focused on system development – Multiple versions of the system: abstract machine -> refiniements -> implementation – The proofs are for the consistency between versions • Syntax is expressed using mathematical symbols or their ASCII equivalents (e.g. ! for ∀) • Lots of syntactic sugar for easily writing down expressions Language features • Types: based on set theory Types are either basic (integer, bool, string, enum) or built using Cartesian product, power set or record – – – – – – – Types inferred by typing predicates (∈, ⊂, ⊆, =) The type of something is „the biggest set that contains it” The type of integer literals and expressions is ℤ The type of a set literal or expression is p(set), e.g. ℤ ∈ p(ℤ) The type of a function from X to Y is ℘(X × Y) Distinction of „concrete” types that can be used in implementation Many advanced types such as array, sequence, relation, tree – each with their own set of operators Language features • Expressions and predicates – Predicates use the syntax of first order logic – Expressions of various types use the types’ specific operators – Lambda expressions are allowed • Substitutions – – – – – Allow a predicate to be transformed ( [x := E] P ) Resemble features of an imperative language Also some „alien” features (precondition etc.) Proof obligations are derived from substitutions Can be nondeterministic (but the implementation must be deterministic, cf. concrete types) Language features • Some types of substitution – – – – – – – – – – – – BEGIN…END skip := :() :∈ PRE ASSERT IF CASE LET VAR ; || WHILE Language features • Machine – The „thing” that we are reasoning about – Resembles classes from OOP – Can be abstract, refinement or implementation – Special constraints apply to implementations – Elements of a machine: • • • • Parameters and their constraints Imports, sees, includes etc. Sets (enum or „deferred”) Abstract and concrete constants, variables Language features – Elements of a machine • Properties, invariants • Values (!) • Initialisation and operations – expressed as a substitution • Operations can have multiple return values • Assertions – this makes it possible to use B as a mathematical proof assistant Language features Example: adding assertions to help with a proof. MACHINE MA CONCRETE_VARIABLES var Typing predicate INVARIANT var ∈ INT ⋀ var2 = 1 This must be proven from the invariant. ASSERTIONS Then it can be used as a lemma in other proofs. var = 1 ⋁ var = - 1 ... END Language fetaures • The B0 language – Restricted version of the B language – Used for implementation only – Substitutions are equivalent to instructions – Translated to C(++), Ada etc. The Prover • Atelier B uses both an automatic and interactive prover • The basic concept is the proof obligation (PO): Goal + hypotheses • The prover doesn’t type check – that’s part of the proof! e.g. b = e1 + e2 where b ∈ BOOL and e1 ∈ ℤ, e2 ∈ ℤ is a legal goal which is unprovable • Well-definedness must be proved too e.g. 8/c is well-defined if c ≠ 0 The Prover • Proof obligations – The types of things match up – The refinements are consistent – The initialisation sets the invariants and the operations keep them – The operations meet their pre/postconditions – Assertions are true The Prover • Rules: inductive, deductive and rewriting • Theory: a list of rules (higher index has priority) • Tactic: a list of theories to search for an applicable rule – Backward tactic divides the goal into subgoals – Forward tactic generates new hypotheses – A full tactic is the combination of the two The Prover • Procedure of applying the tactic: – Search the backward tactic for an applicable rule – If one is found, apply it and continue with the next theory – Tilde (~) can be used as the „repeat” operator – The whole tactic is implicitly tilded – For every new hypothesis generated, run the forward tactic with the same procedure The Prover • The theory is fully customizable, even with inconsistent rules! • The prover might loop infinitely • Proof obligations are normalized – Examples: n > m becomes m+1 <= n, a ⇔ b becomes (a ⇒ b) ∧ (b ⇒ a), a ⊆ b becomes a ∈ ℘(b) The Prover • Commands can be given to the interactive prover • The prover will try to prove what is needed to execute the command. If it fails, a new goal is created • ae : Abstract expression – P[…, expr, …] after ae(expr, y) becomes well-defined(expr) ∧ expr=y ⇒ P[…, y, …] Commands • ah: Add Hypothesis – If the goal was h1, …, hn ⇒ G, ah(P) replaces it with h1, …, hn ⇒ P h1, …, hn, P ⇒ G • ct: proof by contradiction – Replaces a goal h1, …, hn ⇒ G with h1, …, hn, ¬ G ⇒ bfalse Commands • dc: Do Cases – If the goal is G, use dc(P) to split it into ¬P⇒G P⇒G • se: Suggest for Exist – If the goal is∃(w1, …, wn).P(w1, …, wn) se(v1, …, vn) turns it into P(v1, …, vn) Commands • ap: Arithmetic Proof – An automated mechanism for proving things about systems of linear equations and inequations • pp: Predicate Prover – Another automated system • pr: Prover Call – Yet another (these all solve different kinds of goals) • ar: Apply Rule – Just applies a rule • dd: Deduction – For a goal P ⇒ Q, raise P in the hypothesis stack then prove Q • ba: Back • cg: display Current Goal • qu: Quit Demo • The task: decide if a given number is prime Creating a project Adding a component • Let’s add something to the empty project… Adding a component • Since this is our first component, the only choice is „Machine”. Editing • Now that we have a machine, double click it on the „Components” list to edit Insert Theorem Here • What we want to enter there: MACHINE prim OPERATIONS p ← is_prim ( n ) = PRE n ∈ [3 .. MAXINT] THEN p := bool (∀ i . ( i ∈ [ 2 .. n-1 ] ⇒ ( n mod i ) ≠ 0 ) ) END END Insert Theorem Here • What it will look like in B: Atelier B hates singleletter identifiers so we reduplicate everything Adding an implementation IMPLEMENTATION prim_i REFINES prim OPERATIONS pp <-- is_prim ( nn ) = BEGIN VAR ll , kk IN ll := TRUE ; kk := nn ; WHILE ( 2 /= kk & ll = TRUE) DO IF nn mod (kk-1) = 0 THEN kk := kk-1; ll := FALSE ELSE kk := kk-1 END INVARIANT ll : BOOL & nn : NAT & nn >= 3 & kk : 2..nn & (ll=TRUE => (! jj.(jj:kk..nn-1 => nn mod jj /=0))) & (ll=FALSE=> ( kk: 2..nn-1 & nn mod kk = 0)) VARIANT kk END ; pp :=ll END END END Generate PO’s • Click „Po”, then „F0” to try to prove… Interactive Proof time! Interactive Prover Double-click one Interactive Prover • Now we can enter commands. Completing the proof Here are the commands to complete the proof: dc(jj = kk-1) pr ah(jj: kk..nn-1) pp(100) pr dc(ll$7777 = TRUE) dd ah(kk$7777 = 2) pr pp pr dd ah(ll$7777 = FALSE) pp dd pr se(kk$7777) pr Completing the proof • Green means success! THE END