Please enable JavaScript.
Coggle requires JavaScript to display documents.
L016, L020 - Coggle Diagram
L016
How to structure a B project?
Imports
implementation only
blocks imports with machines with same var
must be implemented as a tree (no cycles)
toplevel is an exception
Sees
Sees gives access in RO Mode
No modification operation can be used
Not transitive
e.g.
M1
M2: sees M1
M2: sees M2
doesn't see M1
LOCAL_OPERATION
not exported
L020
Managing Projects
Modeling
Generates Proof Obligations (PO)
Prooving
Proof Obligations
Automatic proof
~[70;85]% mean value
Proof Obligations
False PO
~10%
Must fix B model
Interactive Proof
~ 16 PO/day
Generating code
Generated only after modeling and proof
Aspects
modularity and maintenability
Proof aspect
High number of proof obligations
must simplify the model
Complex proofs
must simplify the model
Library
Must be used from same workspace
Workspaces
Defines a set of elements