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