Please enable JavaScript.

Coggle requires JavaScript to display documents.

The B-Method: L14, L15 - Coggle Diagram

- - - - Structure:
        
        REFINES (mandatory);
        
        IMPORTS, SEES, PROMOTES (structuring);
        
        SETS and their PROPERTIES;
        
        CONCRETE_VARIABLES and their INVARIANT;
        
        CONCRETE_CONSTANTS (CONSTANTS) and their VALUES.
      - B0 substitutions
        
        skip
        
        Assignments
        
        Sequence
        
        Alternation
        
        Case
        
        Loops
        
        Blocks
        
        Operations calls of imported machines
        
        Read-only operations calls of seen machines
      - B0 expressions
        
        Itertifier or literal constant
        
        Access to an elements of an array
        
        bool ( cond )
      - B0 predicates
        
        Conjunction
        
        Disjunction
        
        Negation
        
        Comparison
      - B0 types
        
        Scalar types
        
        NAT
        
        INT
        
        BOOL
        
        Defined or enumerated SETS
        
        Arrays
      - B0 values
        
        Concrete constants and defined sets have to be valued