Abstract Machine Notation

Overview

This description of the Abstract Machine Notation is organised as follows:-

Some constructs require the use of a type-determining predicate to be well-formed. A type-determining predicate P must contain a constraining predicate of the form xx: S, xx < S, xx <: S or xx = E, where xx\S, xx\E.

AMN Substitutions

The generic syntactic variables are as follows: P, Q, R for predicates; S, T, U, V for AMN substitutions, E,F for expressions; ff, xx, yy for variables; l, m, n for lists of expressions; vlx for variable lists; opn for AMN operation names; asub for AMN substitutions. z\E indicates that there are no free occurrences in E of the variables in z. The definitions below are given in terms of Generalised Substitutions. The syntax is presented informally, and occurrences of `...' mean that any number of the surrounding construct can occur.

 BEGIN S END            =   S

 PRE P THEN S END       =   P | S

 IF P THEN S ELSE T END =   (P ==> S) [] (not(P) ==> T)

 IF P THEN S END        =   IF P THEN S ELSE skip END


 IF P THEN              =   IF P THEN
   S                          S   
 ELSIF Q THEN               ELSE      
   T                          IF Q THEN
 ...                            T
 ELSIF R THEN                 ...
   U                            ELSE
 ELSE                              IF R THEN
   V                                 U
 END                               ELSE
                                     V
                                   END
                                END
                              ...
                            END


 IF P THEN              =   IF P THEN 
   S                          S
 ELSIF Q THEN               ELSIF Q THEN
   T                          T
 ...                        ...
 ELSIF R THEN               ELSIF R THEN
   U                          U
 END                        ELSE
                              skip
                            END


 CHOICE                 =   S [] T [] ... U
   S
 OR
   T
 OR 
  ...
 OR
   U 
 END


 SELECT P THEN          =   P ==> S []
   S                        Q ==> T []
 WHEN Q THEN                ... []
   T                        R ==> U
 ...
 WHEN R THEN 
   U
 END


 SELECT P THEN          =   SELECT P THEN   
   S                          S
 WHEN Q THEN                WHEN Q THEN
   T                          T
 ...                        ...
 WHEN R THEN                WHEN R THEN
   U                          U
 ELSE                       WHEN not(P) & not(Q) & ... & not(R) THEN
   V                          V
 END                        END


 CASE E OF              =   SELECT E: {l} THEN
   EITHER l THEN              S
     S                      WHEN E: {m} THEN
   OR m THEN                  T
     T                      ...
   ...                      WHEN E: {n} THEN
   OR n THEN                  U
     U                      ELSE
   ELSE                       V
     V                      END
   END
 END


 CASE E OF               =  SELECT E: {l} THEN
  EITHER l THEN               S
    S                       WHEN E: {m} THEN
  OR m THEN                   T
    T                       ...
  ...                       WHEN E: {n} THEN
  OR n THEN                   U
    U                       ELSE
  END                         skip
 END                        END

 VAR xx IN               =  @xx.S
   S 
 END         

 ANY xx WHERE P          =  @xx.(P ==> S). P must contain a 
 THEN                        type determining predicate.
   S
 END

 LET xx BE               =  @xx.(xx = E ==> S), where xx\E.
   xx = E
 IN 
   S 
 END


 S || T                     Parallel substitution (S and T are substitutions on 
                            disjoint sets of variables.

 xx:= E || yy:= F       =   xx,yy:= E,F

 opn                        An AMN substitution, with name opn.

 opn(vl1)                   A parameterised AMN substitution, with input vl1.

 vl2 <-- opn                A parameterised AMN substitution, with output vl2.

 vl2 <-- opn(vl1)           A parameterised AMN substitution, with input vl1 and
                            output vl2.


 xx:= bool(P)           =   IF P THEN 
                              xx:= TRUE
                            ELSE
                              xx:= FALSE
                            END


 skip                       No-op

 xx:: E                   =  @xx'(xx': E ==> xx:= xx')

 xx: P                    =  @xx'.([xx:= xx']P ==> xx:= xx'). P must contain a 
                             type determining predicate.


 ff(xx):= E               =  ff:= ff <+ {xx|->E}

 S;T                         Identical to its Generalised Substitution
                             counterpart, S;T.


 S;WHILE P DO             =  S, followed by looping on T so long as the guard P 
     T                       holds, with loop variant E and loop invariant Q.
   INVARIANT                   
     Q
   VARIANT
     E
   END

AMN Operations

The generic variables are as follows: vlx for variable lists; opn for operation names; asub for AMN substitutions. AMN operations have the following forms:

 opn = asub

 opn(vl1) = asub

 vl2 <-- opn = asub

 vl2 <-- opn(vl1) = asub

Abstract Machines

Abstract Machine constructs are described by the following BNF-like syntax; the order in which optional clauses appear is not significant.

Here, the syntax
exp1 | exp2 indicates exp1 or exp2 (choice),
< exp > indicates zero or one occurrence of exp (optionality) and
<< exp >> indicates zero or more occurrences of exp (repetition).

Identifier, UpperCaseIdentifier, Rule, Bnumber, Formula and ProgramLikeFormula are as defined in the section on the B-Platform and in the B-Tool Reference Manual.

Machines

  MACHINE             Identifier < ( param_list ) >

  < CONSTRAINTS       Formula << & Formula >> >    

  < USES              rnm_machine_ref  << , rnm_machine_ref >> >      

  < SEES              rnm_machine_ref  << , rnm_machine_ref >> > 

  < INCLUDES          rnm_machine_ref < ( param_list ) > 
                      << , rnm_machine_ref < ( param_list ) > >> >

  < PROMOTES          rnm_operation_ref << , rnm_operation_ref >> >

  < EXTENDS           rnm_machine_ref < ( param_list ) >
                      << , rnm_machine_ref < ( param_list ) > >> >

  < SETS              UpperCaseIdentifier << ; UpperCaseIdentifier >> > |
                      enumerated_set << ; enumerated_set >> >

  < CONSTANTS         Identifier << , Identifier >> >

  < PROPERTIES        Formula << & Formula >> >

  < VARIABLES         Identifier << , Identifier >> >

  < INVARIANT         Formula << & Formula >> >

  < ASSERTIONS        Formula << & Formula >> >

  < DEFINITIONS       Formula == Formula << ; Formula == Formula >>
 
  < INITIALISATION    Formula >

  < OPERATIONS        operation < ; operation >> >

  END


  param_list        ::=  Identifier << , Identifier >>


  enumerated_set    ::=  UpperCaseIdentifier = { set_contents } 


  set_contents      ::=  Identifier << , Identifier >> > |
                         Bnumber << , Bnumber >>

  rnm_machine_ref   ::=  < rename_prefix . > Identifier 


  rnm_operation_ref ::=  < rename_prefix . > Identifier


  rename_prefix     ::=  Identifier


  operation         ::=  < param_list <-- > Identifier < ( param_list ) >
                            = ProgramLikeFormula

Refinements

  REFINEMENT          Identifier  

  REFINES             machine_ref

  < SEES              machine_ref  << , machine_ref >> > 

  < SETS              UpperCaseIdentifier << ; UpperCaseIdentifier >> > |
                      enumerated_set << ; enumerated_set >> >

  < CONSTANTS         Identifier << , Identifier >> >

  < PROPERTIES        Formula << & Formula >> >
 
  < VARIABLES         Identifier << , Identifier >> >

  < INVARIANT         Formula << & Formula >> >

  < ASSERTIONS        Formula << & Formula >> >

  < DEFINITIONS       Formula == Formula << ; Formula == Formula >>
 
  < INITIALISATION    Formula >

  < OPERATIONS        operation < ; operation >> > 

  END


  param_list     ::=  Identifier << , Identifier >>


  enumerated_set ::=  UpperCaseIdentifier = { set_contents } 


  set_contents   ::=  Identifier << , Identifier >> > |
                      Bnumber << , Bnumber >>


  machine_ref    ::=  Identifier 


  operation_ref  ::=  Identifier


  operation      ::=  < param_list <-- > Identifier < ( param_list ) >
                        = ProgramLikeFormula

Implementations

  IMPLEMENTATION      Identifier 

  REFINES             machine_ref

  < SEES              machine_ref  << , machine_ref >> > 

  < IMPORTS           machine_ref < ( act_param_list ) > 
                      << , machine_ref < ( act_param_list ) >> > >

  < PROMOTES          operation_ref << , operation_ref >> >

  < SETS              UpperCaseIdentifier << ; UpperCaseIdentifier >> > |
                      enumerated_set << ; enumerated_set >> >

  < CONSTANTS         Identifier << , Identifier >> >

  < PROPERTIES        Formula << & Formula >> >

  < INVARIANT         Formula << & Formula >> >

  < ASSERTIONS        Formula << & Formula >> >

  < DEFINITIONS       Formula == Formula << ; Formula == Formula >>
 
  < INITIALISATION    Formula >

  < OPERATIONS        operation < ; operation >> > 

  END


  param_list     ::=  Identifier << , Identifier >>


  act_param_list ::=  act_param << , act_param >>


  act_param      ::=  Bnumber | Identifier | Formula | 
                      Bnumber .. Bnumber | { set_contents }


  enumerated_set ::=  UpperCaseIdentifier = { set_contents } 


  set_contents   ::=  Identifier << , Identifier >> > |
                      Bnumber << , Bnumber >>


  machine_ref    ::=  Identifier

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo