Skip to main content
Department of Information Technology

Provably Correct Software, Spring -11

The String machine

We have written a machine Str to implement strings. Strings are represented as elements of the set seq(0..255), that is sequences of character codes (integers from 0..255). You can naturally use strings in your specification using built-in B operators such as ^ and /|\. The Str machine stores one string in a variable with the name ss so that is what you would use in your implementation machine invariant when you refer to the string. If you need several strings, you import the machine with renaming.

Strings are assumed to have a maximum length given by the constant strMaxLength. The implementation of Str currently sets this constant to 1000, which should be enough for most situations.

The Str machine has an "export" format of strings which is used when an operation needs to return a string as a value or pass a string as an argument. This format is a fixed size array with indices 0..strMaxLength where the element with index 0 is the length of the string and the characters of the string are stored in elements with index 1 and up. You should not (need to) manipulate this "export" format. If you need an array of strings, then you can create your own array (or the ones in the Atelier B standard library) and store the "export" format of the strings there.

Note that the Str machine is not to be included in specification machines. It should be imported into an implementation machine. The Str machine is in the STR library project in Atelier B. You must add that project as a library in the same way as you add the standard library LIBRARY. (See the page on using Atelier B.)

The following operations are available in the Str machine.

  • read: One line of text (or at most strMaxLength characters) is read from standard input and stored in the string. Note that in the specification this is given as an nondeterministic assignment of an arbitrary value to the string. This is because the input comes from the outside world -- we don't know anything about it.
  • write: The string is written to standard output. Note that in the specification this is given as a do nothing-operation. This is because output only affects the outside world -- not the B machines.
  • nn <--strSize: nn is set to the currentlength of the string.
  • cc <-- getChar(nn): cc is set to the character at position nn. (Positions start at 1.)
  • set(aa): The string is set to aa. (aa is a string in the "export" format.)
  • aa <-- get: aa is set to the "export" format of the string.
  • aa <-- substring(yy,ll): aa is set to the substring of length ll beginning at position yy. (aa is in "export" format.)
  • append(aa): aa is appended to the string. (aa is a string in the "export" format.

The code of the Str machine

MACHINE Str
DEFINITIONS string(s) == (s:0..strMaxLength-->NAT & s(0) <= strMaxLength & ran((1..strMaxLength)<|s) <: 0..255)
ABSTRACT_CONSTANTS arrSeq
CONSTANTS strMaxLength
PROPERTIES strMaxLength : NAT &
           arrSeq: (0..strMaxLength --> NAT) --> seq(0..255) &
           arrSeq = %aa.(aa:(0..strMaxLength --> NAT) | 1..aa(0) <| aa)
VARIABLES ss
INVARIANT ss : seq(0..255) & size(ss) <= strMaxLength
INITIALISATION ss := <>
OPERATIONS
  read = ANY ss1 WHERE ss1 : seq(0..255) & size(ss1) <= strMaxLength
         THEN ss := ss1
         END;

  write = skip;

  nn <-- strSize = nn := size(ss);

  cc <-- getChar(nn) = PRE nn:NAT1 & nn <= size(ss) THEN
                           cc := ss(nn)
                       END;

  setChar(nn, cc) = PRE cc:0..255 & nn:NAT1 & nn <= size(ss) THEN
                        ss(nn) := cc
                    END;
  
  set(aa) = PRE string(aa) THEN
               ss := arrSeq(aa)
             END;

  aa <-- get = ANY aa1 WHERE string(aa1) & ss=arrSeq(aa1) THEN
                   aa := aa1
                END;

  aa <-- substring(yy, ll) = PRE yy : NAT1 & yy <= size(ss) & ll : NAT & (yy+ll) : 1..(size(ss)) THEN
                                 ANY aa1 WHERE string(aa1) & (ss \|/ (yy-1)) /|\ ll = arrSeq(aa1) THEN
                                    aa := aa1
                                 END
   			      END;
 
 append(aa) = PRE string(aa) & size(ss) + aa(0) <= strMaxLength THEN
                 ss := ss^arrSeq(aa)
              END  

END

Updated  2011-01-17 11:04:03 by Lars-Henrik Eriksson.