Provably Correct Software, Spring -10

Problems with Atelier B

There are some bugs and restrictions in Atelier B or its documentation. This web page explains such problems that we have found.

This information refers to version 3.7.1 of Atelier B which we are using in the course.

Missing/incorrect information in the Reusable Components Reference Manual

• A machine which uses L_SEQUENCE should not SEE the machines BASIC_ARITHMETIC and BASIC_BOOL. There are no such machines...
• The library machine L_PFNC for implementing partial functions is missing from the manual. You can read its B specification machine instead.
• The library machine L_RELATION for implementing general relations is missing from the manual. You can read its B specification machine instead.

Code generator gives incorrect code for array values

If an operation returns an array, you will get a error when you try to compile the resulting C program. There is a reasonably simple workaround. Contact an instructor if you get this problem.

The B0 language type checking is syntactic

When checking that array types are compatible -- e.g. in an assignment statement setting one array variable to the value of another -- the B0 checker makes a syntactic check. E.g. the two array types 1..2*3 --> NAT and 1..6 --> NAT are considered different!

For the same reason, the B0 checker will not detect that the argument or result value of an operation is implementable ("concrete") unless it can be determined syntactically. E.g.

MACHINE Abstr
VARIABLES ss
INVARIANT ss<:NAT
INITIALISATION ss:={}
OPERATIONS
  add(nn) = PRE nn:NAT THEN ss:=ss\/{nn} END;
  remove(nn) = PRE nn:ss THEN ss:=ss-{nn} END;
  nn <-- pick = PRE ss/={} THEN nn::ss END
END

The argument to remove is concrete as it is a member of ss and all members of ss are members of NAT. However, this can not be determined syntactically but only by reasoning on the type of ss.

Workaround: add a redundant type condition to the precondition of remove:

  remove(nn) = PRE nn:NAT & nn:ss THEN ss:=ss-{nn} END;

Similarly, the B0 checker can not determine that the return value of pick is concrete. This time the workaround is more clumsy. (If you can find a better one, please tell me!)

  nn <-- pick = PRE ss/={} THEN ANY xx WHERE xx:NAT & xx:ss THEN nn:=ss END END

By the explicit condition that xx:NAT, the B0 checker can tell that the return value is concrete.

The B0 language checker makes unnecessary complaints about abstract data

In some cases the B0 checker requires that arguments (and presumably also the value) of an operation must be implementable ("concrete") even if the operation itself is not going to be implemented! This can happen if you have a structure such as this:

  MACHINE Op 
  OPERATIONS 
    rr <-- op(ss) = PRE ss:seq(INT) THEN rr:=size(ss) END 
  END 

  MACHINE Opref 
  INCLUDES Op 
  OPERATIONS 
  rr <-- opref(aa,ll) = 
              PRE aa:1..10-->INT & ll:0..10 THEN rr <-- op(1..ll<|aa) END 
  END 

  IMPLEMENTATION OprefI 
  REFINES Opref 
  OPERATIONS 
    rr <-- opref(aa,ll) = rr:=ll 
  END 

Here op is not an operation of the machine Opref so it should not be implemented by OprefI. Still, the B0 checker complains that the argument of op is a sequence, which is not an implementable data structure.

Avoid an excessive number of proof obligations

Atelier B will construct proof obligations for each path through a program. If you are not careful, you can write the progam so that there are many "impossible" paths, which will still get their own proof obligations. This can lead to long processing times or even to the capacity of Atelier B to be exceeded. Take for instance the following program fragment:

  IF aa < 0 THEN
    ....
  END;
  IF aa = 0 THEN
    ...
  END;
  IF aa > 0 THEN
    ...
  END;

In each IF there are two alternative paths, depending on the truth value of the test. So in all there are 2*2*2=8 paths through this program fragment. In general, if you have N IF-statements in sequence, you will get 2**N possible paths. Note that in this example only 3 of the 8 paths can actually be taken since the tests are mutually exclusive (assuming that aa is not modified inside the IF-statements). Instead, write the program in the following way:

  IF aa < 0 THEN
    ....
  ELSE IF aa = 0 THEN
    ...
  ELSE
    ...
  END;

Now you use ELSE-branches and nested IF-statements instead of a sequence and you will only get 3 paths!

Another possibility is to use a CASE-statement.

USES may force unnecessary promotions

Consider the following set of machine fragments:

MACHINE M1
INCLUDES M2,M3
OPERATIONS
  foo = bar
END

MACHINE M2
USES M3
END

MACHINE M3
OPERATIONS
  bar = skip
END

Atelier B will fail to generate proof obligations for M1, claiming that bar is undefined. It appears that when a machine (M2 in this case) USES another machine (M3 in this case), their common ancestor machine (M1 in this case) can not access operations in its included machines (bar in this case)! This problem does not happen if M2 SEES M3 and is likely due to a bug in the mechanism for generating proof obligations for the USES clause -- such proof obligations appear in the closest common ancestor machine.

Workaround: promote the operations you use (in this case add a PROMOTES bar clause to M1. Then Atelier B will work correctly at the expense of getting extra proof obligations for the unnecessarily promoted operations -- proof obligations that may not even hold! If they don't you'll just have to live with having a few unprovable proof obligations. (Proof obligations for bar in M1 in this case.)