🧑‍🎓
Training Resources for Atelier B
  • Introduction
  • Guides and Tutorials
    • Installation
    • Training Videos
    • Training Slides
    • Applying the B Method
      • Project Creation
      • Code Generation
      • Mathematical Proof
        • 🔥Writing Mathematical Rules
          • Introduction
          • Introduction to the Theory Language
          • How to write mathematical rules
          • Using Automatic Prover Mechanisms
          • Guards in a nutshell
          • Normalisation of Expressions
          • Common pitfall
          • All guards in the theory language
    • Extending Atelier B
      • Syntax
      • Examples
    • Programming the CLEARSY Safety Platform
  • Examples and Case-studies
    • Fuel Level
    • Switch
    • Security Policy
    • Verified Software Competitions
  • Additional Resources
    • Glossary
    • References
    • Frequently Asked Questions
Powered by GitBook
On this page

Was this helpful?

  1. Guides and Tutorials
  2. Applying the B Method
  3. Mathematical Proof
  4. Writing Mathematical Rules

Guards in a nutshell

This chapter presents succinctly the different kinds of guards that are available to write mathematical rules (for further details, see Appendix C). For each guard, the following elements are presented:

  • syntax,

  • possibly its semantics,

  • a textual description of its behaviour.

It must be noted that certain guards have a mathematical semantics only under special circumstances (e.g. the bsearch guard).

The following guards may be employed to obtain one or several hypothesis from the stack, by processing first the most recently inserted hypothesis.

Syntax
Semantics

bgetallhyp(H)

H

bgethyp(H)

H

binhyp(H)

H

The following guard checks if s is an element of STRING.

Syntax
Semantics

bstring(s)

s : STRING

The following guard checks if P is a conjunction.

Syntax
Semantics

bpattern(P, (Q & R))

P <=> (Q & R)

The bsearch guard has a mathematic semantics when the list in which the search is performed is the argument list of an associative and commutative operator. This is the case for the operators &, or, / and /. This is also the case of the operator , (comma) for a list of quantified variables. One must thus check that the application of the rule remains within such cases.

Syntax
Semantics

bsearch(N, (P, Q), M)

(P, Q) = (M, N)

bsearch(N, (P & Q), M)

(P & Q) <=> (M & N)

bsearch(d, (a or b), c)

(a or b) <=> (c or d)

bsearch(d, (a / b), c)

a / b = c / d

bsearch(d, (a / b), c)

a / b <=> c / d

The following guard succeeds if t is true and has the form a op b.

Syntax
Semantics

btest(t)

t

The following guard checks if n is a numeric value both positive and smaller or equal to maxint.

Syntax
Semantics

n : NATURAL

The following guard succeeds if both arguments succeed.

Syntax
Semantics

band(P, Q)

Semantics of P and semantics of Q

The role of the following guards is to verify the relationship between wildcards representing variables and wildcards representing expressions.

Syntax
Semantics

bvrb(x)

x

blvar(x)

x

x P

x (if x P)

bfresh(x, P, y)

y (if y P)

PreviousUsing Automatic Prover MechanismsNextNormalisation of Expressions

Last updated 3 years ago

Was this helpful?

🔥