🧑‍🎓
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

Common pitfall

What is an infinite loop of the prover?

For instance, consider applying the rule:

a * a == a * a * a / a

on the following goal

cc(v) = vv * vv

We will obtain successively the following goals:

cc(v) = vv * vv * vv / vv
cc(v) = (vv * vv * vv / vv) * vv / vv
...

The kernel of the prover then produces the following messageskrt: sequence memory short

krt: asking for 1500000 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
krt: asking for 2249997 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
 krt: asking for 3374992 int, waiting for system reply...
krt: OK, memory obtained, we continue.
...

The messages krt: sequence memory short are generated by the kernel when it dynamically claims additional memory.

This example is simple. Infinite loops may be caused by combination of rule applications and be more difficult to detect a priori.

PreviousNormalisation of ExpressionsNextAll guards in the theory language

Last updated 3 years ago

Was this helpful?

🔥