Home

reusable_components_..

1. preconditions jj and kk must be in 0 LAC_maxidx jj lt kk and vv be in LAC minval LAC maxval For implementation location reasons kk must not equal the MAXINT constant outputs TRUE if an element that is greater or equal to vv was found FALSE if not iiis a NAT if bb TRUE then ii is the smallest index in the image array that is greater than or equal to vv Search for an element that is greater than or equal to vv in jj kk starting from jj ASCENDING SORT ARRAY syntax ASCENDING_SORT_ARRAY ii jj preconditions ii and jj must be in 0 LAC_maxidx For implementation reasons ii and jj must not equal MAXINT Shift sort in ascending order the smallest first on the ii jj portion IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY VAR machine clause IMPORTS BASIC ARRAY VAR Therefore if another instance is required it must be given a different instance name for example il BASIC ARRAY VAR DESCRIPTION OF LIBRARY MACHINES 37 5 5 L_PFNC Partial Function OPERATIONS VAL_PFNC value of the function for an element in its domain STR PENC overloads the partial function with a pair XST_PFNC test that an index is in the partial function domain RMV PFNC removes a pair from the partial function SET_PFNC overloads
2. REVERSE_RGE EXAMPLE array reverse the order of the elements in part of an array The following example is a machine that represents the color assigned to 101 dots for each array in a range this color may be red green or blue for each dot A operation enables finding a red dot in an array 52 Reusable Components Reference Manual MACHINE m3 IMPLEMENTATION SETS m3 1 COLOR red green blue REFINES VARIABLES m3 color IMPORTS INVARIANT il L ARRAY3 RANGE 0 10 100 COLOR color 0 10 0 100 COLOR INVARIANT INITIALISATION il arr rge color color 0 10 x 0 100 x red INITIALISATION OPERATIONS il SET_ARR_RGE 0 0 100 red ii bb find_red rng PRE il DUP_ARR_RGE 1 10 0 rng 0 10 A OPERATIONS rouge ran color rng ii bb find_red rng vAR bb IN THEN ii bb ii color rng red ilL SEARCH MAX EQL RGE rng 0 100 red bb c BOOL END END END END DESCRIPTION L ARRAY3 RANGE is the most complete of the two dimensional array machines with no constraintf This makes it possible to create arrays with values that are the elements of an enumerated set while retaining access to complete operations such are reversing the order of elements The operation that is not available is the one that would require an order relation on the elements in the array sort MACHINE PARAMETERS L ARRAY3 RANGE LATR_minrge LATR maxrge LATR maxidx LATR VALUE The range interv
3. PCMP_SEQ_RGE syntax idx bb PCMP SEQ RGE rngl ii jj rng2 kk preconditions rngl and rng2 must be in the LSR_minrge LSR_maxrge range ii and jj must be valid indexes in the rng1 and ii jj position sequences kk must be a valid index in the rng2 position sequence kk jj ii must be a valid index in the rng2 position sequence output bb is TRUE if there is an element of the ii jj part in the seq rge rngl sequence that is different to the kk kk jj ii part of the seq rge rng2 sequence FALSE if not idx is a NAT if bb is TRUE the idx represents the index of the first element that is different in the seq rge rngl ii jj sequence Partial comparison of two sequences IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY RANGE and BASIC ARRAY VAR machines Therefore if other in stances are required they must be given a name that is not blank example i1l BASIC ARRAY RANGE DESCRIPTION OF LIBRARY MACHINES 67 5 12 L ARRAY COLLECTION collection of arrays of the same size OPERATIONS CRE_ARR_COL returns a Boolean element that indicates that there remains an array available in the collection and gives the index of this available array DEL_ARR_COL VAL_ARR_COL STR_ARR COL COP ARR COL CMP A
4. ARRAY write an element promoted operation SET ARRAY write the same value in a portion of the table promoted opera tion SWAP ARRAY exchange two elements promoted operation RIGHT SHIFT ARRAY shift a portion to the large index promoted operation LEFT SHIFT ARRAY shift a portion to the small index promoted operation SEARCH MAX EQL ARRAY search for a value in a portion of the table promoted operation SEARCH MIN EQL ARRAY search for a value in a portion of the table promoted operation REVERSE ARRAY invert the order of elements in a portion of the table promoted operation SEARCH MIN GEQ ARRAY search for the first element that exceeds a value pro moted operation ASCENDING SORT ARRAY sort of a table portion L PFENC partial function VAL PFNC value of the function for an element in its domain STR PENC overloads the partial function with a couple XST_PFNC tests if an index is in the partial function domain RMV_PFNC removes a couple from the partial function SET PFNC overloads a part of the function with a constant SWAP PFNC exchanges the images for two domain indexes RIGHT SHIFT PFNC right shift of a domain part LEFT SHIFT PFNC left shift of a domain part SEARCH MAX EQL PFNC searches for a value in the partial function SEARCH MIN EQL PFNC searches for a value in the partial function REVERSE PFENC reverses the order of elements for a portion of the domain INDEX OF LIBRARY MACHINES 7
5. ASCENDING_SORT_PFNC sorts in a portion of the domain L_SEQUENCE building a sequence LEN_SEQ returns the current size of the sequence IS_FULL_SEQ is used to determine if the sequence is full size LS_maxsize IS_INDEX_SEQ is used to determine whether ii is a valid index VAL_SEQ value of an element in the sequence FIRST_SEQ returns the first element in the sequence LAST_SEQ returns the last element in the sequence PUSH_SEQ add vv to the end of the sequence POP_SEQ removes the last element from the sequence its value is lost STR_SEQ changes the value of an element in the sequence RMV_SEQ removes an element from the middle of the sequence INS_AFT_SEQ inserts vv right after index ii CLR_SEQ clears the sequence TAIL_SEQ removes the first element from the sequence KEEP SEQ only keeps the first elements in the sequence CUT SEQ cuts the nn first elements from the sequence PART SEQ only retains part ii jj in the sequence REV SEQ reverses the order of elements in the sequence FIND FIRST SEQ finds vv in the sequence from the start FIND LAST SEQ finds vv in the sequence from the end L SET creating a set CARD SET returns the cardinal for the set IS FULL SET identifies if the set is full card LSET_maxsize IS INDEX SET identifies if a number is a valid index VAL SET value of a element in the set FIND SET finds an element in the set RMV SET removes an element from the set INS SET inserts an
6. FALSE if not rr is a NAT if bb TRUE then rr is the smallest index in the rng array equal to vv Search for an element in an array that is equal to vv by scanning the ii jj part starting from ii REVERSE_RGE syntax REVERSE_RGE rng ii jj preconditions rng must belong to LAT R minrge LATR maxrge ii and jj belong to 0 LATR maxidx Reversing the order of elements in the ii jj part of the rng array DESCRIPTION OF LIBRARY MACHINES 55 IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC_ARITHMETIC BASIC_BOOL WARNING The implementation of this machine creates the default instance for the BASIC_ARRAY_RANGE machine IMPORTS BASIC_ARRAY_RANGE clause Therefore if another instance is necessary it must be given a non empty instance name for example il BASIC ARRAY RANGE 56 Reusable Components Reference Manual 5 10 L ARRAY5 RANGE Range of Arrays of the Same Size with Ordered Value Numerical Indexes Sort Operation OPERATIONS VAL ARR RGE value of an element promoted operation STR ARR RGE write an element promoted operation COP ARR RGE copy an array to another promoted operation CMP ARR RGE compare two arrays promoted operation DUP ARR RGE duplicate the same array to a set of arrays promoted operation SET_ARR_RGE copy the same value to an index range in one of the arrayx pro moted operation PCOP_ARR_RGE cop
7. INT WRITE print an integer BOOL READ operator input of a Boolean TRUE or FALSE state BOOL WRITE print TRUE or FALSE CHAR READ operator input of a character CHAR WRITE print a character STRING WRITE print a message SIMPLE EXAMPLE The following implementation displays hello on the terminal IMPLEMENTATION bonj 1 REFINES MACHINE bonj bonj IMPORTS OPERATIONS BASIC IO main skip OPERATIONS END main BEGIN STRING WRITE helloWin END END DESCRIPTION BASIC IO is used for simple input output actions on a terminal This basic machine is used to build models Such I O cannot be considered as safe In UNIX the system devices used are standard input and standard output stdin and stdout they can therefore be redirected INTERVAL READ syntax bb INTERVAL_READ mm nn preconditions mm and nn must be NATs so that mm lt nn outputs bb integer in mm nn The operator inputs an integer of the interval mm nn The input format forces to type a succession of number s followed by RETURN The first input character must be a number On the opposite case the input fails 3 is not valid When a character that is not the first input is not a number anymore this character as all the following ones are ignored 3e2 is a valid input of the integer 3 As long as the input is false the message THIS IS NOT A NUMBER IN mm nn is displayed and a new entry is required DESCRIPTION OF BASIC MACHIN
8. LACR_maxidx The ii jj part of the rng array is compared with the part of the same size in the rng2 array The idx2 jj ii 0 LACR_maxidx condition guarantees that this comparison is possible bb is a Boolean element that is FALSE if the two parts are equal and TRUE if they are different In the latter case idx is the index of the first element that is different from ii jj DESCRIPTION OF LIBRARY MACHINES 59 SWAP_RGE syntax SWAP RGE rng jii jj preconditions rng is in LACR_minrge LACR_maxrge ii and jj in 0 LACR_maxidx The ii and jj elements in the array are exchanged RIGHT_SHIFT_RGE syntax RIGHT_SHIFT_RGE rng ii jj nn preconditions rng must belong to LACR_minrge LACR_maxrge ii jj and nn belong to 0 LACR_maxidx with ii lt jj and jj nn lt LACR_maxidx to allow the shift right by nn spaces The ii nn jj nn part of the rng array receives a copy of the ii jj part from this same array shift nn spaces to the right LEFT_SHIFT_RGE syntax LEFT_SHIFT_RGE rng ii jj nn preconditions rmg must belong to LACR_minrge LACR_maxrge ii and jj belong to 0 LACR_maxidx with ii lt jj nn must belong to NAT with nn lt ii to make possible the left shift by nn spaces For implementation reasons jj cannot equal MAXINT The ii nn jj nn part of the rng array receives a copy of the ii jj part of this same array shift nn spaces to the left SEARCH MAX EQL RGE syntax rr bb SEARCH MAX EQL RGE rng jii jj vv prec
9. allow either the creation of dynamic arrays that cannot be obtained using BO or producing models using vt100 style inputs outputs dynamics arrays are arrays which size depends on the machine parameters Such arrays cannot be realised directly in BO the safety design of the ADA C and C translators do not allow to treat this case For example the following construction is not allowed IMPLEMENTATION mm xx CONCRETE_VARIABLES mytab INVARIANT mytab 0 xx NAT END Such an array would have to be realised using BASIC_ARRAY_VAR The atelier actual version is composed of three basic machines BASIC_ARRAY_VAR Arrays with dimension 1 BASIC_ARRAY_RGE Arrays with dimension 2 BASIC_IO Usual inputs outputs management This chapter presents this three machines The basic machine BASIC_IO is intended to the model designing It mustn t be considered as safe WARNING The manual implementations of the basic machines BASIC_ARRAY_VAR and BASIC_ARRAY_RGE destined for the translators supplied with Atelier B are pro vided as demonstration They are not safe and are not appropriated in all the B use contexts 14 Reusable Components Reference Manual 4 1 BASIC_ARRAY_VAR Implanting a one dimensional table OPERATIONS VAL_ARRAY read a table element STR_ARRAY write a table element EXAMPLE Example of use with listed sets MACHINE array SETS FONTS Times Serif Courier FTYPE fixed unfix
10. be in 0 LPF_maxidx with ii lt jj and jj nn lt LPF_maxidx to allow the right shift by nn spaces It is also necessary for ii jj to be included in the domain of the partial function The ii nn jj nn part is overloaded by a copy of the ii jj part in the partial function shift by nn spaces to the right LEFT_SHIFT_PFNC syntax LEFT_SHIFT_PFNC ii jj nn preconditions ii jj must be in 0 LPF_maxidx with ii lt jj nn must be a NAT with nn lt ii to allow the left shift by nn spaces In addition it is necessary for ii jj to be included in the domain of the partial function The ii nn jj nn part is overloaded by a copy of the ii jj part in the partial function shift left by nn spaces SEARCH MAX EQL PFNC syntax rr bb SEARCH MAX EQL PFNC ijj vv preconditions ii and jj must be in 0 LPF maxidx ii jj and vv be in LPF_minval LPF _maxval outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the largest index the image of which by the partial function is vv Search for an array element that equals vv by scanning the ii jj part starting from jj SEARCH MIN EQL PFNC syntax rr bb SEARCH_MIN_EQL_PFNC ii jj vv preconditions ii and jj must be in 0 LPF_maxidx ii lt jj and vv be in LPF_minval LPF _maxval outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the smallest index the image of which by the partial function is vv Search for an array el
11. element in the set CLR SET clears all elements from the set L ARRAY 1 RANGE array of tables of the same size with numerical indexes VAL ARR RGE value of an element promoted operation Reusable Components Reference Manual STR ARR RGE COP ARR RGE CMP ARR RGE DUP ARR RGE SET ARR RGE PCOP ARR RGE PCMP ARR RGE write an element promoted operation copy a table to another promoted operation compare two tables promoted operation duplicate the same table into a series of tables copy the same value to an index set in one of the tables copy part of one of the tables to a different table to a given posi tion find the first element that is different from two parts of two tables A Boolean element indicates if this element was found and in this case the index of this element is returned L ARRAY 3 RANGE range of tables of the same size with numerical in dexes and values that are not ordered maximum operations VAL ARR RGE STR ARR RGE COP ARR RGE CMP ARR RGE DUP ARR RGE SET ARR RGE PCOP ARR RGE PCMP ARR RGE SWAP RGE value of an element promoted operation write an element promoted operation copy a table to another promoted operation compare two tables promoted operation duplicate the same table to an array of tables promoted opera tion copy the same value to a range in one of the tables promoted operation copy part of one of the t
12. element of a sequence gives the last element of a sequence adds an element to a sequence removes the last element from a sequence changes the value of an element in a sequence removes an element from a sequence the size of which is reduced by 1 adds an element to a sequence the size of which increases by 1 empties a sequence removes the first element from a sequence only retains the first N in a sequence elements cuts the N first elements from a sequence only retains in a sequence the indexes between the two limit values reverses the order of the elements in a sequence FIND FIRST SEQ RGE searches for a value in a sequence returns a Boolean element indicating whether it was found and if yes returns the smallest corresponding index FIND LAST SEQ RGE searches for a value in a sequence returns a Boolean element COP SEQ RGE CMP SEQ RGE PCOP SEQ RGE PCMP SEQ RGE indicating whether it was found and if yes returns the largest corresponding index copies one of the sequences to another compares two sequences partial copy from one sequence to another partial comparison of two sequences 62 Reusable Components Reference Manual EXAMPLE The example below shows the use of LSEQUENCE_RANGE on a numbered set IMPLEMENTATION sr_l rete REFINES sr E classical baroque rock rap funk IMFORTS MARIAHERS SISTERE SNR sl L SEQUENCE RANGE 1 5 10 ST E INVARIANT sl seq rge vv
13. is a BOOL idx is in ii jj The ii jj part in array nnl is compared to part idx2 idx2 jj ii in array nn2 bb is FALSE if the two parts are identical TRUE if not In this case idx is the index of the first element that is different from ii jj IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL
14. of possible values for array elements 0 LAT_maxidx is the set of array indexes VAL_ARRAY syntax vv VAL_ARRAY ii preconditions ii must be in 0 LAT_maxidx outputs vv is a LAT_VALUE it is the value of the array at position ii STR_ARRAY syntax STR ARRAY ii vv preconditions ii must be in 0 LAT_maxidx and vv must belong to LAT VALUE The vv value is stored in the array at index ii SET ARRAY syntax SET_ARRAY ii jj vv preconditions ii jj must be a subset of 0 LAT_maxidx and vv belong to LAT VALUE For implementation reasons it is also necessary that jj be different from MAXINT The vv value is stored in the array for all indexes between ii and jj If ii gt jj the array will not change SWAP ARRAY syntax SWAP_ARRAY ii jj preconditions iijj must be in 0 LAT_maxidx The ii and jj elements in the array are exchanged RIGHT_SHIFT_ARRAY syntax RIGHT_SHIFT_ARRAY ii jj nn preconditions ii jj nn must be in 0 LAT_maxidx with ii lt jj and jj nn lt LAT_maxidx to make possible the possible the shift to the right by nn spaces Part ii4 nn jj4 nn receives a copy of part ii jj of the array shift nn spaces to the right LEFT_SHIFT_ARRAY syntax LEFT_SHIFT_ARRAY ii jj nn preconditions iijj must be in 0 LAT_maxidx with ii lt jj nn must be NAT with nn lt ii to make possible the shift to the left by nn places For implementation reasons jj must be not equal MAXINT The ii nn jj nn part receives a copy
15. the LAUR minrge LAUR maxrge interval the index interval is 0 LAUR_maxidx and LAUR VALUE is the set of possible values VAL ARR RGE syntax vv VAL_ARR_RGE range index preconditions range must belong to LAUR minrge LAUR maxrge and index belong to 0 LAUR maxidx outputs vv is a LAUR VALUE it is the value of the array range at the index position STR ARR RGE syntax STR_ARR_RGE range index value preconditions range must belong to LAUR_minrge LAUR_maxrge index belong to 0 LAUR maxidx and value belong to LAUR VALUE The value data value is stored in the indexed array range COP ARR RGE syntax COP_ARR_RGE dest src preconditions dest and src are in LAUR_minrge LAUR_maxrge The src array is copied to the dest array CMP ARR RGE syntax bb CMP_ARR_RGE rangel range2 preconditions rangel and range2 are in LAUR minrge LAUR maxrge outputs bb is a BOOL element that is TRUE if the two arrays are equal and FALSE if not SET ARR RGE syntax SET_ARR_RGE range ii jj vv preconditions range must belong to LAUR_minrge LAUR_maxrge ii jj be included in 0 LAUR maxidx and vv belong to LAUR VALUE For implementation reasons jj must also be different from MAXINT The vv value is stored in the array range for all index values between ii and jj If ii gt jj the array remains unchanged DUP ARR RGE syntax DUP_ARR_RGE dest1 dest2 src preconditions destl dest2 src are in LAUR minrge LAUR ma
16. using CRE ARR COL VAL ARR COL Syntax vv VAL ARR COL ii jj Preconditions ii must belong to 1 LACOLL_maxobj and jj belong to LACOLL INDEX Output vv contains the jj number value of array ii Use vv to store the value of number jj in array ii STR_ARR_COL Syntax STR ARR COL ii jj vv Preconditions ii must belong to 1 LACOLL_maxobj jj belong to LACOLL INDEX and vv belong to LACOLL VALUE Write the value of vv to cell number jj in array ii COP ARR COL Syntax COP ARR COL dest src Preconditions dest and src must belong to 1 LACOLL_maxobj Copy the contents of the src array to the dest array CMP ARR COL Syntax bb CMP ARR COL range 1 range 2 Preconditions range 1 and range 2 must belong to 1 LACOLL_maxobj Output bb is a Boolean element indicating whether array range 1 and range 2 are identical Comparison between the two 2 arrays IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC_ARITHMETIC BASIC_BOOL DESCRIPTION OF LIBRARY MACHINES 69 5 13 L_ARRAY1_COLLECTION array of the same size with nu merical indexes OPERATIONS CRE_ARR_COL DEL_ARR_COL VAL_ARR_COL STR_ARR COL COP_ARR_COL CMP_ARR_COL SET_ARR COL PCOP_ARR_COL PCMP_ARR_COL EXAMPLE returns a Boolean element indicating whether an array remains available in the collection and the index of this available array promoted operation rel
17. 0 LSET_maxsize Returns the size of the set IS FULL SET syntax bb IS FULL SET output bb is TRUE if the set is full FALSE if not States whether the set is full size LSET_maxsize IS INDEX SET syntax bb IS_INDEX_SET ii preconditions ii must be a NAT outputs bb is TRUE if ii is an index of the set FALSE if not States whether ii is a valid index VAL_SET syntax vv VAL SET ii preconditions ii must be an index of the set ii 1 size seq_vrb outputs vv is the value of the ii the element vv LSET VALUE Value of an element of the set FIND SET syntax bb ii FIND SET vv preconditions vv must be in LSET VALUE outputs bb is TRUE if vv is in the set FALSE if not ii is a NAT if bb TRUE then it indicates the position of element vv Search for vv in the set RMV SET syntax RMV SET vv preconditions vv must be in the set Removes an element from the set 47 DESCRIPTION OF LIBRARY MACHINES INS_SET syntax INS SET vv preconditions vv must be in LSET VALUE Adds an element to the end of the set if it is not already in it if not it does nothing CLR SET syntax CLR_SET Clears the set 48 Reusable Components Reference Manual 5 8 L_ARRAY1_ RANGE A Range of Arrays of the Same Size with Numerical Indexes OPERATIONS VAL_ARR_RGE STR_ARR_RGE COP_ARR_RGE CMP_ARR_RGE DUP_ARR_RGE SET_ARR_RGE PCOP_ARR_RGE PCMP_ARR_RGE EXAMPLE Using SET_ARR
18. 1 STR ARRAY 2 1 END Another example Only the implementation is presented The write of a machine refined by this implementation is an exercice for the reader IMPLEMENTATION parr 1 REFINES parr IMPORTS BASIC ARRAY VAR FONTS FTYPE VALUES FONTS 5 7 FTYPE 3 4 INVARIANT arr_vrb fixedsz INITIALISATION STR ARRAY 5 3 STR ARRAY 6 4 STR ARRAY T 5 END NOTE The possible values of the BASIC ARRAY VAR parameters are given by the B language rules refer to section 12 2 page 574 of the BBOOK DESCRIPTION OF BASIC MACHINES 17 4 2 BASIC_ARRAY_RGE Implementing a Two Dimensional Ar ray OPERATIONS VAL_ARR_RGE STR_ARR_RGE read an array element write an array element COP_ARR_RGE copy an array line to another CMP_ARR_RGE compare two array lines EXAMPLE Example of use two lines and three columns array MACHINE bitab SETS LGNS 111 112 VARIABLES mytab INVARIANT mytab LGNS 1 3 0 255 INITIALISATION mytab lll 1 7 2 8 3 9 l2 gt 15 02 1335 2H END IMPLEMENTATION bitab 1 REFINES bitab IMPORTS BASIC ARRAY RGE I 3 0 255 LGNS INVARIANT arr rge mytab INITIALISATION STR ARR RGE IIL 1 7 STR ARR RGE I STR ARR RGE I STR ARR RGE I n wl 0 STR ARR RGE II2 STR ARR RGE ID 3 2 END J Jj 9 js 1 The variable arr_rge is the name of the encapsulated array par BASIC_ARRAY_
19. ASIC ARRAY VAR and BASIC ARRAY RGE destined to the translators supplied with Ate lier B are provided as a demonstration They are not safe and not appropriate in all the B use context In the case of a more complete use the user would have to realize these basic machines 26 Reusable Components Reference Manual 5 1 L_ARITHMETIC1 Extended Integer Operations The integer term refers to the elements of NAT NAT that is the set of the natural integers between 0 and MAXINT OPERATIONS MIN minimum of two integers MAX maximum of two integers INC increment an integer strictly inferior to MAXINT DEC decrement a literal integer EXP exponentiation SQRT default integer square root LOG_BY_DEFAULT default logarithm LOG_BY_EXCESS logarithm by excess EXAMPLE The example below shows a machine that uses a certain number of functionalities of the machine L ARITHMETICI MACHINE IMPLEMENTATION ml ml 1 OPERATIONS REFINES Xx opl ANY tt WHERE ml tt NAT A ttxtt 16 IMPORTS THEN L ARITHMETICI xx tt OPERATIONS END XX opl BEGIN xx op2 ANY tt WHERE xx SQRT 16 tt NAT A 3 27 END THEN XX op2 VAR rr IN xx tt xx rr LOG BY DEFAULT 3 27 END END END END DESCRIPTION L ARITHMETICI offers arithmetical operations such as roots and logarithms operations on the elements NAT and dedicated to calculatory applications Calculus being integers values the search operat
20. Atelier B Reusable Components Reference Manual version 3 6 F eL bh A CLEARSY SYSTEM ENGINEERING ATELIER B Reusable Components Reference Manual version 3 6 Document made by CLEARSY This document is the property of CLEARSY and shall not be copied duplicated or distributed partially or totally without prior written consent All products names are trademarks of their respective authors CLEARSY ATELIER B Maintenance Europarc de PICHAURY 1330 Av J R Guilibert Gauthier de la Lauziere Bat C2 13856 Aix en Provence Cedex 3 France Tel 33 0 4 42 37 12 99 Fax 33 0 4 42 37 12 71 Email maintenance atelierbQ clearsy com CONTENTS iii Contents IL Introduction 1 2 Index of Basic Machines 3 3 Index of Library Machine 5 4 Description of Basic Machine 13 14 es pee ue us 4 3 BASIC I O vt100 styleinputs outputg lees 20 Description of Library Machine 25 26 D _ARRAYI One Dimensional Array with Initialization Loop 29 D ARRAYS Array with Non Ordered Values Maximum Operations 31 5 4 _ARRAY5 Array with Ordered Values Sort Operation 34 D 6 L SEQUEN Creating a Sequence 41 5 E Creating 960 9 x oc we on hoe RR e he hes RR xo ed eoe ao OR Value Numerical Indexes sort Operatio nigh how ale OM om Beers ae 200 5 11 L SEQUENCE RAN Range of Sequences 61 ARRAY Q ON collection of arrays of the sa
21. DING SORT RGE 0 0 4 vv yy xx gt vv yy xx 1 REVERSE_RGE 0 0 4 END DUP_ARR_RGE 1 20 0 END DESCRIPTION L_ARRAY5_RANGE is the most complete two dimensional array machines It especially contains a sort operation implanted by a shift sort fast algorithm MACHINE PARAMETERS L ARRAY5 RANGE LACR minrge LACR maxrge LACR maxidx LACR_minval LACR_maxval LACR_minrge LACR_maxrge is the set of ranges 0 LACR maxidx is the set of indexes and LACR_minval LACR_maxval the set of possible values All of the parameters must be NATs this machine does not allow negative values In addition LACR_minrge LACR_maxrge 1 lt LACR_maxidx and LACR_minval lt LACR_maxval VAL ARR RGE syntax vv VAL ARR RGE range index preconditions range must belong to LACR_minrge LACR_maxrge index belong to 0 LACR_maxidx outputs vv is a LACR_VALUE it is the value of the array range at the index position STR ARR RGE syntax STR_ARR_RGE range index value preconditions range must be in LACR_minrge LACR_maxrge index must be in 0 LACR_maxidx value must belong to LACR VALUE The value of the value element is stored in the array range as an index 58 Reusable Components Reference Manual COP_ARR_RGE syntax COP_ARR_RGE dest src preconditions dest and src are in LACR_minrge LACR_maxrge The src array is copied to the dest array CMP ARR RGE syntax bb CMP_ARR_RGE rangel rang
22. ES 21 INT_WRITE syntax INT_WRITE vv preconditions vv must belong to NAT Output number vv with no return BOOL_READ syntax bb BOOL_READ outputs bb must be Boolean The operator enters Boolean TRUE or FALSE conditions with no character before it for example TRUE is rejected because of the space before it As long as the operator has not made a valid entry the message THIS IS NOT A BOOL VALUE type TRUE or FALSE is displayed and a new entry is required BOOL WRITE syntax BOOL WRITE bb preconditions bb must be Boolean Output TRUE or FALSE with no return CHAR READ syntax cc CHAR READ outputs cc must be part of 0 255 Operator entry of a character that is interpreted as a number in 0 255 Type in the character followed by return If several characters has been typed only the first one is taken into account example cdef is understood as 32 In C pressing Return only returns 10 ctrl D EOF returns 0 In ADA only the visible characters entries i e no control characters are accepted CHAR WRITE syntax CHAR WRITE vv preconditions vv must belong to the range 0 255 Displays the cc character on screen example CHAR WRITE 10 to produce a return Remember a single quote means prime the language s notation conventions and B CHAR WRITE A for example means nothing On the contrary the quoted strings are valid elements in a formula they serve for STRING WRITE be
23. INVARIANT INITIALISATION vv 1 5 seq ST A Vrr rr 1 5 size vv rr lt 10 s1 LR BEQ ROE s1 PUSH SEQ RGE 1 baroque INTTIA LISA TION s1 PUSH_SEQ_RGE 1 rock vv 1 5 x baroque rock rap s1 PUSH_SEQ_RGE 1 rap OPERATIONS s1 COP SEQ RGE 2 1 ii bb trouve rap rng PRE s1 COP_SEQ_RGE 3 1 Mi Eus sl COP SEQ RGE 4 1 s1 COP SEQ RGE 5 1 ii c vv rng rap OPERATIONS Be BOOL ii bb trouve rap rng BEGIN END bb ii s1 FIND FIRST SEQ RGE rng rap END END DESCRIPTION L SEQUENCE RANGE enables implementing and using a set number of sequences with a fixed maximum size The sequence number evolves in a range that is a machine parameter the maximum size of all of the sequences is also a machine parameter The purpose is to be able to make comparisons and copies between these sequences directly using an additional operation to the traditional operations on each of the sequences MACHINE PARAMETERS L SEQUENCE RANGE LSR_minrge LSR_maxrge LSR_maxsize LS8R VALUE the variable is a total function of LSR minrge LSR maxrge in the set of VALUE sequences with a maximum size of LSR_maxisize LEN SEQ RGE syntax nn LEN SEQ RGE range preconditions range must belong to the LSR minrge LSR maxrge range outputs nn is the size of the range position nn 0 LSR maxsize Gives the size of a sequence DESCRIPTION OF LIBRARY MACHINES 63 IS FULL SEQ
24. PLEMENTATION mil_1 sa DE REFINES ml linis IMPORTS il L_ARRAY1 0 255 10 per pr 0 255 INVARIANT INITIALISATION arr_urb is the variable in L ARRAY1 0 10 x 5 il arr_vrb vv CR i INITIALISATION il SET ARRAY 0 10 5 END DESCRIPTION As it is possible L ARRAYI is used instead of BASIC ARRAY VAR L ARRAYIL re alises using an array an abstract variable representing a function It is then possible to have an initialization operation of the entire function or of a part of it initialization loop The starting part of the function performed is an interval if not it would not be possible to indicate a portion of this set without mentioning all elements involved MACHINE PARAMETERS L ARRAYI LAU VALUE LAU maxidx LAU VALUE is the set of possible values for the array elements 0 L AU maxidx is the set of array indexes VAL ARRAY syntax vv VAL_ARRAY ii preconditions ii must be in 0 LAU_maxidx outputs vv is an element of LAU_VALUE the array value at position ii 30 Reusable Components Reference Manual STR_ARRAY syntax STR ARRAY ii vv preconditions ii and vv must belong to the 0 LAU maxidx and LAU VALUE respec tively vv value is stored in the array at ii index SET ARRAY syntax SET ARRAY ii jj vv preconditions ii jj is a sub set of 0 LAU maxidx and vv an element of LAU VALUE For implementation reasons f jj and MAXINT must be different The value vv is stored in the array for al
25. RGE DESCRIPTION BASIC_ARRAY_RGE models two dimensional arrays Such arrays cannot be created directly in BO if their size depends on the machine parameters dynamic array The safe design of the ADA C or C translators do not allow to treat this case The following construction is forbidden IMPLEMENTATION mm xx mytab INVARIANT END CONCRETE_VARIABLES mytab 0 10 0 xx x 0 xx 18 Reusable Components Reference Manual Such an array must be implemented using BASIC ARRAY RGE MACHINE PARAMETERS BASIC ARRAY RGE BAR INDEX BAR VALUE BAR RANGE BAR INDEX represents the column indexes BAR VALUE is the set of the possible values for the array elements BAR RANGE represents the line indexes The B language rules concerning the possible values of the BAR VALUE parameter ensure that a computing variable being able to contain the ele ments of MININT MAXINT then it can contain those of BAR VALUE For example the B rules do not permit to give to BAR VALUE the value MAXINT 1 MAXINT 4 2 VAL ARR RGE syntax vv VAL ARR RGE rrjii preconditions ii must be a BAR INDEX rr must be BAR RANGE outputs vv is an element of BAR_VALUE which value is the array value at po sition ii line rr STR_ARR_RGE syntax STR_ARR_RGE rr ii vv preconditions rr must be an element of BAR RANGE ii an element of BAR INDEX and vv an element of BAR VALUE Value vv is stored in
26. RGE syntax bb IS_FULL_SEQ_RGE range preconditions range must belong to the range LSR_minrge LSR_maxrge outputs bb is TRUE if the range position sequence is full FALSE if not Indicates whether a sequence is full IS_INDEX SEQ RGE syntax bb IS INDEX SEQ RGE range ii preconditions range must belong to the LSR minrge LSR maxrge range ii must be a NAT outputs bb is TRUE if ii is an index in the range position sequence FALSE if not Identifies whether an integer is in a sequence domain VAL SEQ RGE syntax vv VAL_SEQ_RGE range ii preconditions range must belong to the LSR_minrge LSR_maxrge range ii must be an index in the range position sequence ii 1 size seq_rge range outputs vv is the value of the ii th element in the range position sequence vv VALUE Gives the value of a sequence for a valid index FIRST_SEQ RGE syntax vv FIRST SEQ RGE range preconditions range must belong to the LSR_minrge LSR_maxrge range the range position sequence must not be empty outputs vv is the value of the first element in the range position sequence vv VALUE Gives the first element in a sequence LAST SEQ RGE syntax vv LAST SEQ RGE range preconditions range must be in the LSR minrge LSR maxrge range the range position sequence must not be empty outputs vv is the value of the last element in the range position sequence vv VALUE Gives the last eleme
27. RR COL releases the specified array read an element from one of the valid arrays write an element from one of the valid arrays copy one of the arrays to another compare two arrays EXAMPLE IMPLEMENTATION M11 REFINES MACHINE M1 ml IMPORTS OPERATIONS L_ARRAY_COLLECTION 4 1 10 1 10 iil ii2 initialise arrayx vv PRE OPERATIONS vv 1 10 iil ii2 initialise_arrayx vv BEGIN THEN VAR bl b2 IN iil NAT iil bl CRE ARR COL ii2 NAT ii2 b2 CRE ARR COL END STR ARR COL iil l vv END COP ARR COL ii2 iil END END END DESCRIPTION L ARRAY COLLECTION is used to handle identically sized one dimensional arrays It contains basic operations create delete read write compare MACHINE PARAMETERS L ARRAY COLLECTION LACOLL_maxobj LACOLL INDEX LACOLL VALUE LACOLL_maxobj is the maximum number of arrays in the collection LACOLL INDEX is the set of array indexes LACOLL VALUE is the set of possible values of array elements 68 Reusable Components Reference Manual CRE_ARR_COL Syntax ii bb CRE_ARR_COL Outputs bb is a Boolean element indicating whether any available arrays are left in the collection ii is the index of this available array Assigning an array in the collection DER_ARR_COL Syntax DEL ARR COL ii Preconditions ii must belong to 1 LACOLL maxobj The array of index ii in the collection is released It may once again be assigned
28. UE then ii is the smallest index in the image array that exceeds or is equal to vv Search for an element that exceeds or is equal to vv in the jj kk range starting from jj ASCENDING_SORT_RGE syntax ASCENDING_SORT_RGE rng ii jj preconditions rng must belong to LACR_minrge LACR_maxrge ii and jj belong to 0 LACR_maxidx For implementation reasons ii and jj must not be different from MAXINT Shift sort in ascending order starting with the smallest on the ii jj range in an array IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC_ARITHMETIC BASIC_BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY RANGE machine IMPORTS BASIC ARRAY RANGE clause Therefore if another instance is necessary it must be given a non empty instance name for example il BASIC ARRAY RANGE DESCRIPTION OF LIBRARY MACHINES 61 5 11 L SEQUENCE RANGE Range of Sequences OPERATIONS LEN SEQ RGE gives the size of a sequence IS FULL SEQ RGE indicates whether a sequence is full IS INDEX SEQ RGE indicates whether an integer is in the sequence domain VAL SEQ RGE FIRST SEQ RGE LAST SEQ RGE PUSH SEQ RGE POP SEQ RGE STR SEQ RGE RMV SEQ RGE INS SEQ RGE CLR SEQ RGE TAIL SEQ RGE KEEP SEQ RGE CUT SEQ RGE PART SEQ RGE REV SEQ RGE gives the value of a sequence for a valid index gives the first
29. _RGE value of an element promoted operation write an element promoted operation copy an array to another promoted operation compare two arrays promoted operation duplicate the same array to a series of arrays copy the same value to an index interval in one of the arrays copy part of one array to a different array to a given position search for the first element that is different between two parts of two arrays A Boolean element indicates whether this element was found and in this case the index of this element in returned and DUP_ARR_RGE to initialize a set of arrays IMPLEMENTATION ml 1 T Tue REFINES ml Ve IMPORTS T MS 7 DO IAPNCRDUION 255 vv 0 20 0 10 0 255 il arr_rge vv INITIALISATION INITIALISATION vv 0 20 x 0 10 x 5 iLSET ARR RGE 0 0 10 5 END il DUP ARR RGE 1 20 0 END DESCRIPTION L ARRAYI RANGE is used in place of BASIC ARRAY RANGE so that a range of arrays may create a set of function type abstract variables when operations are required to perform complete array initialization It also allows performing operations that use parts of two different arrays The index and range sets are intervals so that it is possible to indicate only portions of these sets without listing all elements involved DESCRIPTION OF LIBRARY MACHINES 49 MACHINE PARAMETERS L_ARRAY1_RANGE LAUR_minrge LAUR_maxrge LAUR_maxidx LAUR_VALUE The range interval is
30. a part of the function with a constant SWAP PFNC exchanges the images for two domain indexes RIGHT SHIFT PFNC right shift part of the domain LEFT SHIFT PFNC left shift part of the domain SEARCH MAX EQL PFNC search for a value in the partial function SEARCH MIN EQL PFNC search for a value in the partial function REVERSE PFENC reverse the order of elements in a portion of the domain ASCENDING SORT PFNC sort in a portion of the domain EXAMPLE IMPLEMENTATION MACHINE ml 1 mi REFINES VARIABLES mi pf IMPORTS INVARIANT L_PFNC 0 255 10 pf 0 10 0 255 INVARIANT INITIALISATION pfnc_vrb pf pf 4 6 INITIALISATION END STR_PFNC 4 6 END DESCRIPTION L_PFNC implements a partial function with almost all of the operations available in L_ARRAY5 In fact only SEARCH_MIN_GEQ is not used The practical usefulness of partial functions is that they dispense with the need to add a non existent or unused element in the input sets in order to implant them as total functions The implementation of L_PFNC performs these elements by using the seldom used MAXINT value MACHINE PARAMETERS L_PFNC LPF_minval LPF_maxval LPF_maxidx LPF minval LPF maxval is the in put set of the function 0 LPF_maxidx is the source set LPF minval LPF_maxval 38 Reusable Components Reference Manual LPF_maxidx must be NATs this machine does not allow negative values Moreover LPF_minval lt LPF_maxval and 1 lt LPF_maxidx as
31. a portion to the small index promoted operation SEARCH MAX EQL ARRAY search for a value in an array promoted operation SEARCH MIN EQL ARRAY search for a value in an array portion promoted opera tion REVERSE ARRAY reverse the order of elements in an array portion EXAMPLE The example below is a machine that represents the color assigned to 101 points this color may be red green or blue for each point An operation is used to find a red dot UM IMPLEMENTATION 11 SETS un COLOR fred green blue xL lr as IMPORTS il L_ARRAY3 COLOR 100 INVARIANT INNARA color 0 100 COLOR Harah toldi ata ee di INITIALISATION Gorn MONG il SET_ARRAY 0 100 red 5 OPERATIONS iibb trouve red PRE 3 scuve e anedon ii bb trouve red HER 8 VAR bb IN ii color red mop moe BodL iL SEARCH MAX EQL ARRAY 0 100 red AND END i END DESCRIPTION L ARRAYS3 is the most complete of the one dimensional array machines that do not require that the output set be part of an interval L ARRAYS has been constrained It is therefore possible to create arrays with values that are elements of a listed set while having access to complete operations such as element order reversal The operation that 32 Reusable Components Reference Manual is not available is the one that would require an order relationship on the array elements sort MACHINE PARAMETERS L_ARRAY3 LAT_VALUE LAT_maxidx LAT VALUE is the set
32. ables to a different table in a given position promoted operation find the first different element from two parts in two tables A Boolean element indicates whether this element was found and in this case the index of this element is returned promoted opera tion swap two elements in a table RIGHT SHIFT RGE shift a table range to the large index LEFT SHIFT RGE shift a table range to the small index SEARCH MAX EQL RGE find the last element that equals a value in a table range SEARCH MIN EQL RGE find the first element that equals a value in a table range REVERSE RGE reverse the order of the elements of a table part L ARRAY 5 RANGE array of tables of the same size with numerical in dexes with ordered values sort operations VAL ARR RGE STR ARR RGE value of an element promoted operation write an element promoted operation INDEX OF LIBRARY MACHINES 9 COP_ARR_RGE copy a table to another promoted operation CMP_ARR_RGE compare two tables promoted operation DUP_ARR_RGE duplicate the same table in a range of tables promoted operation SET_ARR_RGE copy the same value to an index range in one of the arrays pro moted operation PCOP_ARR_RGE copy a range from one of the tables to a different table at a given position promoted operation PCMP_ARR_RGE find the first different element in two ranges in two tables A Boolean element indicates that this element was found and in this case t
33. aces The ii nn jj nn part receives a copy of the ii jj part of the array shift right by nn spaces LEFT SHIFT ARRAY syntax LEFT_SHIFT_ARRAY ii jj nn preconditions ii jj must be in 0 LAC_maxidx with ii lt jj nn must bea NAT with nn lt ii to allow the left shift by nn spaces For implementation reasons jj cannot equal MAXINT The ii nn jj nn part receives a copy of the ii jj part of the array shift left by nn spaces 36 Reusable Components Reference Manual SEARCH MAX EQL ARRAY syntax rr bb SEARCH_MAX_EQL_ARRAY ii jj vv preconditions ii and jj must be in 0 LAC_maxidx ii lt jj and vv be in LAC VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the highest index in the array worth vv Search for an array element equal to vv by scanning the ii jj part starting from jj SEARCH MIN EQL ARRAY syntax rr bb SEARCH_MIN_EQL_ARRAY ii jj vv preconditions ii and jj must be in 0 LAC maxidx ii lt jj and vv be in LAC_VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the smallest index in the array worth vv Search for an array element equal to vv by scanning the ii jj part starting from ii REVERSE ARRAY syntax REVERSE ARRAY ii jj preconditions ii and jj must be in 0 LAC maxidx Reverse the order of the elements in the ii jj portion of the array SEARCH MIN GEQ ARRAY syntax ii bb SEARCH_MIN_GEQ_ARRAY jj kk vv
34. al is LATR minrge LATR maxrge the index interval 0 LATR_maxidx and LATR VALUE is the set of possible values VAL ARR RGE syntax vv VAL ARR RGE range index preconditions range must belong to LATR minrge LATR maxrge index belong to 0 LATR maxidx outputs vv is a LATR_VALUE it is the value of the array range at the index position STR ARR RGE syntax STR ARR RGE range index value preconditions range must belong to LATR minrge LATR maxrge index belong to 0 LATR maxidx and value belong to LATR VALUE The LATR VALUE value is stored in the array range in the index L ARRAYS RANGE can only have a finite integer set as range DESCRIPTION OF LIBRARY MACHINES 53 COP_ARR_RGE syntax COP_ARR_RGE dest src preconditions dest and src are in LATR_minrge LATR_maxrge The src array is copied to the dest array CMP ARR RGE syntax bb CMP_ARR_RGE rangel range2 preconditions rangel and range2 are in LATR_minrge LATR_maxrge outputs bb is an BOOL that equals TRUE if the two arrays are equal and FALSE if not SET_ARR_RGE syntax SET_ARR_RGE range ii jj vv preconditions range must belong to LATR minrge L ATR maxrge ii jj be included in 0 LATR maxidx and vv belong to LATR VALUE For implementation reasons jj must also be different to MAXINT Value vv is stored in the array range for all indexes in the range from ii to jj If ii gt jj the array remains unchanged DUP ARR RGE synt
35. an element indicating that there is an array free in the collection and the index of this free array promoted oper ation DEL_ARR_COL releases the listed array promoted operation VAL_ARR_COL read a element from on of the valid arrays promoted operation STR_ARR COL write a element from one of the valid arrays promoted operation COP_ARR_COL copies from one of the arrays to another promoted operation CMP_ARR_COL compares two tables promoted operation SET_ARR_COL copies the same value to an index range in one of the arrays PCOP_ARR_COL copies part of one of the arrays to another to a given position PCMP_ARR_COL find the first different element between the two parts of the two different arrays A Boolean element indicates if this element was found and in this case the index of this element is returned INDEX OF LIBRARY MACHINES 11 L_RELATION complete binary relations op_reset The relation becomes the empty relation op_isFullRelation Returns TRUE only if the cardinal of the relation equals max_nb _2tupple op_add Adds a couple to the relation op_remove Removes a couple to the relation op_cardinal Returns the relation cardinal op belongsTo Checks if a couple is present in the relation lie the number of couple present in the relation 12 Reusable Components Reference Manual DESCRIPTION OF BASIC MACHINES 13 4 Description of Basic Machines The basic machines supplied with Atelier B
36. ax DUP_ARR_RGE dest1 dest2 src preconditions destl dest2 src are in LATR_minrge LATR_maxrge For implementa tion reasons dest2 must also be different to MAXINT The src array is duplicated in all of the arrays of the dest1 dest2 interval PCOP ARR RGE syntax PCOP_ARR_RGE dest idx_dst src ii jj preconditions dest and src must belong to LATR_minrge LATR_maxrge and be dif ferent ii jj be a non empty interval of 0 LATR_maxidx idx dst belong to 0 LATR_maxidx jj be different from MAXINT and idx_dst jj ii belong to 0 LATR_maxidx necessary condition to avoid copy overflow The ii jj part in the src array is copied to the dest array from the idx_dst index PCMP_ARR_RGE syntax idx bb PCMP ARR RGE rng2 idx2 rngl ii jj preconditions rngl and rng2 are in LATR_minrge LATR_maxrge ii jj is a non empty interval of 0 LATR maxidx idx2 and idx2 jj ii are in 0 LATR maxidx The ii j part of array rngl is compared with the part with the same size in array rng2 The idx2 jj ii 0 LATR maxidx condition guarantees that this comparison is possible bb is a Boolean element that is FALSE if the two parts are equal and TRUE if they are different In the latter case idx is the index of the first element that is different to ii jj 54 Reusable Components Reference Manual SWAP_RGE syntax SWAP_RGE rng iijj preconditions rng is in LATR_minrge LATR_maxrge ii and jj in 0 LATR_maxidx The ii and jj elem
37. ce TAIL SEQ RGE removes the first element from a sequence 10 Reusable Components Reference Manual KEEP SEQ RGE only keeps in a sequence the N first elements CUT SEQ RGE cuts the N first elements from a sequence PART SEQ RGE only keeps in a sequence the indexes in a range between two limits REV SEQ RGE reverses the order of the elements in a sequence FIND FIRST SEQ RGE finds a value in a sequence returns a Boolean element indicat ing that it was found and if yes returns the smallest corresponding index FIND LAST SEQ RGE finds a value in a sequence returns a Boolean element indicat ing that it was found and if yes returns the largest corresponding index COP SEQ RGE copies from one sequence to another CMP SEQ RGE comparison of two sequences PCOP SEQ RGE partially copies one of the sequences to another PCMP SEQ RGE partial comparison of two sequences L ARRAY COLLECTION collection of arrays of the same size CRE_ARR_COL returns a Boolean element indicating that there is still an array free in the collection and gives the index of this free array DEL_ARR_COL releases the identified array VAL_ARR_COL reads an element from one of the valid arrays STR_ARR_COL writes an element from one of the valid arrays COP_ARR_COL copies one of the arrays to another CMP_ARR_COL compares two tables L_ARRAY1_ COLLECTION collection of arrays of the same size with numer ical index CRE_ARR_COL returns a Boole
38. ce Manual 5 4 L ARRAY5 Array with Ordered Values Sort Operation OPERATIONS VAL ARRAY value of an element promoted operation STR ARRAY write an element promoted operation SET_ARRAY write the same value to a portion of an array promoted operation SWAP_ARRAY exchange two elements promoted operation RIGHT_SHIFT_ARRAY shift a portion to the large index promoted operation LEFT_SHIFT_ARRAY shift a portion to the small index promoted operation SEARCH_MAX_EQL_ARRAY search for a value in a portion of the array promoted operation SEARCH MIN EQL ARRAY search for a value in a portion of the array promoted operation REVERSE ARRAY reverse the order of the elements in a portion of the array promoted operation SEARCH MIN GEQ ARRAY search for the first element that exceeds a value pro moted operation ASCENDING SORT ARRAY sort a portion of the array EXAMPLE IMPLEMENTATION MACHINE ml1 1 ml REFINES VARIABLES ml vv IMPORTS INVARIANT L ARRAY5 0 255 4 vv 0 4 0 255 INVARIANT Vxx xx 0 3 gt arr vrb vv vv xx gt vv xx 1 INITIALISATION INITIALISATION SET_ARRAY 0 4 50 vv vv 0 4 0 255 A Vxx xx 0 3 gt STR ARRAY 2 10 STR ARRAY 4 30 vv xx gt vv xx 1 ASCENDING SORT ARRAY 0 4 END REVERSE ARRAY 0 4 END DESCRIPTION L_ARRAY5 is the most complete of the one dimensional array machines It especially comprises a sort
39. cution example ATELIER B bio sdfsdf THIS IS NOT A NUMBER IN 0 100 20 this is the value 20 CRUE THIS IS NOT A BOOL VALUE type TRUE or FALSE TRUE this is the value TRUE cvf DESCRIPTION OF BASIC MACHINES 23 this is the value 99 c ATELIER BY NOTE To be completely rigorous nothing ensures that the operator performs all the entries requested The entry loops of the concrete module BASIC_IO c for example do not really implant the specifications of the corresponding operations Possible evolutions It should be possible to define in the machine BASIC_IO abstract variables modeling the inputs outputs it should then be possible to specify the required interactions of the external system The abstract machine that needs to handle inputs outputs will use BASIC_IO notions by SEES or INCLUDES to represent the required interactions 24 Reusable Components Reference Manual DESCRIPTION OF LIBRARY MACHINES 25 5 Description of Library Machines The library machines are all intended for creating mathematical objects except machine L_ARITHMETIC1 that provides certain arithmetical functions The modeled mathemat ical objects are total functions these are machines contain ARR array in their name partial functions machines with the PFNO partial function in their name sets these are machines with the SET set in their name sequences these are machines with the SEQ seque
40. e2 preconditions rangel and range2 are in LACR_minrge LACR_maxrge outputs bb is a BOOL element that is TRUE if the two arrays are equal and FALSE if not SET_ARR_RGE syntax SET_ARR_RGE range ii jj vv preconditions range must belong to LACR minrge LACR maxrge ii jj be included in 0 LACR_maxidx and vv belong to LACR_VALUE For implementation reasons it is also necessary that jj be different from MAXINT The vv value is stored in the array range for all indexes between ii and jj If ii gt jj the array remains unchanged DUP_ARR_RGE syntax DUP_ARR_RGE dest1 dest2 src preconditions destl dest2 src are in LACR_minrge LACR_maxrge For implementa tion reasons it is also necessary for dest2 to be different from MAXINT The src array is duplicated to all arrays for the dest1 dest2 range PCOP ARR RGE syntax PCOP ARR RGE dest idx_dst src ii jj preconditions dest and src must be different elements of LACR_minrge LACR_maxrge ii jj be a non empty subset of 0 LACR maxidx and idx dst belong to 0 LACR_maxidx jj is different from MAXINT and idx dst jj ii belong to 0 LACR maxidx condition to avoid copy overflow The ii jj range in the src array is copied to the dest array for the idx dst index PCMP ARR RGE syntax idx bb PCMP_ARR_RGE rng2 idx2 rng1 ii jj preconditions rngl and rng2 are in LACR_minrge LACR_maxrge ii jj is a non empty range 0 LACR_maxidx idx2 and idx2 jj ii are in 0
41. eases the array mentioned promoted operation read an element from one of the valid arrays promoted operation write an element from one of the valid arrays promoted opera tion copy one of the arrays to another promoted operation compare two arrays promoted operation copy the same value to an index range in one of the arrays copy part of one of the arrays to another in a given position search for the first different element between two parts of two different arrays A Boolean element indicates whether the element was found and in this case the index of this element is returned Using SET_ARR_COL to fill in two arrays and PCOP_ARR_COL to define a third one Note the need to test the Boolean output elements from CRE ARR COL in order to use the arrays created The example is as follows MACHINE M1 OPERATIONS op skip END 70 Reusable Components Reference Manual IMPLEMENTATION M1_1 REFINES M1 IMPORTS L_ARRAY1_COLLECTION 3 3 1 10 OPERATIONS op VAR i1 i2 13 b1 b2 b3 IN il bl CRE ARR COL i2 b2 CRE ARR COL i3 b3 CRE ARR COL IF bl TRUE A b2 TRUE A b3 TRUE THEN SET_ARR_COL i1 0 3 1 SET_ARR_COL i2 0 3 2 PCOP_ARR_COL i3 0 i1 0 1 PCOP_ARR_COL i3 2 i2 2 3 END END END DESCRIPTION L_ARRAY1_COLLECTION enables the use of a collection of arrays without the need to code loops to position a set of elements or arrays This was not poss
42. econditions ii must be a BAV INDEX outputs vv is a BAV VALUE the value of the array at position ii STR ARRAY syntax STR ARRAY ii vv preconditions ii must be a BAV INDEX and vv must be a BAV VALUE The value vv is stored in the array at ii index C LANGUAGE In C the array is realised by an integer array The accesses to this array are done using method that refuse the index used between 0 and the array size guaranting an optimal memory use The array is dynamically reserved when launching the program If the size indicated by the formal parameters is too big the program stops with the following message Cc Virtual memory exceede in new C LANGUAGE The realisation in C is based on the same principles as in C The stop message on initial reservation failure is Fatal error Malloc of X bytes failed Execution of current application is aborted ADA LANGUAGE The use of generic packaging guarantees an optimal memory occupation No restrictions are made on the instanciation parameters On initial reservation failure an exception stops the program 16 Reusable Components Reference Manual PROGRAMMING Example of use with literal sets IMPLEMENTATION narr 1 MACHINE REFINES narr narr VARIABLES IMPORTS myvar BASIC ARRAY VAR O 2 0 1 INVARIANT INVARIANT myvar 0 2 0 41 arr vrb myvar INITIALISATION INITIALISATION myvar 0 gt 0 1 1 2 1 STR ARRAY 0 0 END STR ARRAY 1
43. ed VARIABLES fixedsz INVARIANT fixedsz FONTS FTYPE INITIALISATION fixedsz Times unfixed Serif fixed Courier fixed IMPLEMENTATION array 1 REFINES array IMPORTS BASIC ARRAY VAR FONTS FTYPE INVARIANT arr vrb fixedsz INITIALISATION STR ARRAY Times unfixed STR ARRAY Serif fixed STR ARRAY Courier fixed END END arr vrb is the name of the table encapsulated by BASIC ARRAY VAR DESCRIPTION BASIC ARRAY VAR modelizes one dimensional arrays Such arrays cannot be created directly in BO if their size dependend on the machine parameters dynamic arrays The current design of ADA or C translators does not allow handling this case The following construction is therefore illegal IMPLEMENTATION mm xx VARIABLES mytab INVARIANT mytab 0 xx NAT END This kind of table should be generated using BASIC ARRAY VAR MACHINE PARAMETERS BASIC ARRAY VAR BAV INDEX BAV VALUE BAV INDEX is the set of values used to index the table BAV VALUE is the set of possible values for table elements DESCRIPTION OF BASIC MACHINES 15 The B language rule relating to the possible values of the BAV VALUE parameter ensure that if a computer variable can contain elements of MININT MAXINT then it can contain those of BAV VALUE For example B rules forbid assigning BAV VALUE the value of MAXINT 1 MAXINT 2 VAL ARRAY syntax vv VAL ARRAY ii pr
44. ement that equals vv by scanning the ii jj part starting from ii REVERSE_PFNC syntax REVERSE PFNC iijj preconditions ii and jj must be in 0 LPF_maxidx and ii jj must be included in the domain of the partial function Reverse the order of the elements in the ii jj portion of the partial function ASCENDING SORT PFNC syntax ASCENDING SORT PFNC iijj preconditions ii and jj must be in 0 LPF_maxidx and ii jj must be included in the domain of the partial function Shift sort in ascending order the smallest first in the ii jj portion 40 Reusable Components Reference Manual IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY VAR machine clause IMPORTS BASIC ARRAY VAR Therefore if another instance is necessary it must be given a different instance name for example il BASIC ARRAY VAR DESCRIPTION OF LIBRARY MACHINES 41 5 6 L SEQUENCE Creating a Sequence OPERATIONS LEN_SEQ returns the current size of the sequence IS_FULL_SEQ shows whether the sequence is full size LS_maxsize IS_INDEX_SEQ shows whether ii is a valid index VAL_SEQ value of an element in the sequence FIRST_SEQ returns the first element in the sequence LAST_SEQ returns the last element in the sequence PUSH_SEQ adds vv to the
45. end of the sequence POP SEQ removes the last element from the sequence its value is lost STR SEQ changes the value of an element in the sequence RMV SEQ removes an element from the middle of the sequence INS AFT SEQ inserts vv right after index ii CLR SEQ clears the sequence TAIL SEQ removes the first element from the sequence KEEP SEQ only keeps the nn first elements in the sequence CUT SEQ cuts the nn first elements from the sequence PART SEQ only keeps the ii jj portion in the sequence REV SEQ reverses the order of the elements in the sequence FIND FIRST SEQ searches for vv in the sequence starting from the beginning FIND LAST SEQ searches for vv in the sequence starting from the end EXAMPLE The example below shows the use of L SEQUENCE for a listed set MACHINE IMPLEMENTATION ml 1 ml SETS REFINES ST classic baroque mi VARIABLES IMPORTS vv L_SEQUENCE 10 ST INVARIANT peto vous seq_urb is the variable in L SEQUENCE ST seq vrb vv bres INITIALISATION INITIALISATION PUSH_SEQ baroque L SEQUENCE guarantees vv baroque baroque ee RRRS that the sequence is empty at the start 42 Reusable Components Reference Manual DESCRIPTION L_SEQUENCE provides a sequence type variable the maximum size of which is a machine parameter Conventional search and shift functions are provided for the practical use of this sequence This answers the frequent problem in programmin
46. ent STR_ARR_RGE write a table element COP_ARR_RGE copy a table line to another CMP_ARR_RGE compare two table lines BASIC IO vt 100 style input output MIN minimum of two numbers MAX maximum of two numbers INC increment a number DEC decrement a number EXP exponential SQRT integer square root by default LOG_BY_DEFAULT logarithm by default LOG_BY_EXCESS logarithm by excess L_ARRAY1 one dimensional table with initialization loop VAL ARRAY value of an element promoted operation STR ARRAY write an element promoted operation SET ARRAY write the same value in a portion of the table L ARRAYS table with non ordered values maximum operations VAL ARRAY value of an element promoted operation STR ARRAY write an element promoted operation SET_ARRAY write a same value in a table portion promoted operation SWAP ARRAY exchange two elements promoted operation RIGHT SHIFT ARRAY shift a portion to the large index promoted operation 6 Reusable Components Reference Manual LEFT SHIFT ARRAY shift a portion to the small index promoted operation SEARCH MAX EQL ARRAY search for a value in a portion of the table promoted operation SEARCH MIN EQL ARRAY search for a value in a portion of the table promoted operation REVERSE ARRAY invert the order of the elements in a portion of the table L ARRAYS table with ordered values sort operation VAL ARRAY value of an element promoted operation STR
47. ents in the array are exchanged RIGHT_SHIFT_RGE syntax RIGHT_SHIFT_RGE rng ii jj nn preconditions rng must belong to LATR minrge L ATR maxrge ii jj and nn belong to 0 LATR maxidx with ii lt jj and jj nn lt LATR_maxidx to allow a right shift by nn spaces The ii4 nn jj4 nn part in the rng array receives a copy of the ii jj part of this same array shift right by nn spaces LEFT SHIFT RGE syntax LEFT_SHIFT_RGE rng ii jj nn preconditions rng is in LATR_minrge LATR_maxrge ii jj must be in 0 LATR_maxidx with ii lt jj nn must be a NAT with nn lt ii to allow the left shift by nn spaces For implementation reasons jj must be equal to MAXINT The ii nn jj nn part of the rng array receives a copy of the ii jj part of this same array shift left by nn spaces SEARCH_MAX_EQL_RGE syntax rr bb SEARCH_MAX_EQL_RGE rngji jj vv preconditions rmg must be in LATR_minrge LATR_maxrge ii and jj must be in 0 LATR maxidx ii lt jj and vv must belong to LATR_VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the largest index in the rng array equal to vv Search for an element in an array equal to vv by scanning the ii jj part starting from jj SEARCH MIN EQL RGE syntax rr bb SEARCH_MIN_EQL_RGE rng ii jj vv preconditions rng must belong to LATR_minrge LATR_maxrge ii and jj belong to 0 LATR maxidx ii lt jj and vv belong to LATR_VALUE outputs TRUE if vv was found
48. even for sequences that are empty or of size 1 FIND_FIRST_SEQ syntax bb ii FIND FIRST SEQ vv preconditions vv must be in VALUE outputs bb is TRUE if vv is in the sequence FALSE if not ii belongs to the range 1 LS_maxsize if bb TRUE then it indicates the first position equal to vv Search for vv in the sequence starting from the start FIND LAST SEQ syntax bb ii FIND LAST SEQ vv preconditions vv must be in VALUE outputs bb is TRUE if vv is in the sequence FALSE if not If bb TRUE ii belongs to the range 1 LS_maxsize and indicates the last position equal to vv Search for vv in the sequence starting from the end IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY VAR machine clause IMPORTS BASIC ARRAY VAR Therefore if another instance is required it must be given a non blank instance name for example il BASIC ARRAY VAR DESCRIPTION OF LIBRARY MACHINES 45 5 7 L_SET Creating a Set OPERATIONS CARD SET returns the cardinal for the set IS FULL SET identifies whether the set is full card LSET maxsize FIND SET finds an element in the set RMV SET removes an element from the set INS SET inserts an element in the set CLR SET removes all of the elements from the set IS INDEX SET ide
49. fault instance for the BASIC ARRAY RANGE machine IMPORTS BASIC ARRAY RANGEY clause Therefore if another instance is necessary it must be given the name of a non empty instance for example il BASIC ARRAY RANGE DESCRIPTION OF LIBRARY MACHINES 51 5 9 L ARRAYS3 RANGE A Range of Arrays of the Same Size with Non Ordered Values Maximum Operations OPERATIONS VAL_ARR_RGE STR_ARR_RGE COP_ARR_RGE CMP_ARR_RGE DUP_ARR_RGE SET_ARR_RGE PCOP_ARR_RGE PCMP_ARR_RGE SWAP_RGE value of an element promoted operation write an element promoted operation copy an array to another promoted operation compare two arrays promoted operation duplicate the same array to a set of arrays promoted operation copy the same value to an index interval in one of the arrays promoted operation copy part of one of the arrays to a different array at a given position promoted operation search for the first element that is different between two parts of two arrays A Boolean element indicates whether this element was found and in this case the index of this element is returned promoted operation exchange two array elements RIGHT_SHIFT_RGE shift part of an array to the large index LEFT_SHIFT_RGE shift part of an array to the small index SEARCH_MAX_EQL_RGE search for the last element that equals a value in part of an array SEARCH_MIN_EQL_RGE search for the first element that equals a value in part of an
50. g applications which is to maintain a list with no blanks MACHINE PARAMETERS L_SEQUENCE LS_maxsize LS_VALUE the variable is a sequence of LS VALUE ele ments with a maximum size that is LS maxsize LEN SEQ syntax nn LEN SEQ outputs 0 LS maxsize Returns the current size of the sequence IS FULL SEQ syntax bb IS FULL SEQ outputs bb is TRUE if the sequence is full FALSE if not Specifies whether the sequence is full size LS maxsize IS INDEX SEQ syntax bb IS_INDEX_SEQ ii preconditions ii must be a NAT outputs bb is TRUE if ii is an index in the sequence FALSE if not Specifies whether ii is a valid index VAL_SEQ syntax vv VAL_SEQ ii preconditions ii must be an index in the sequence ii 1 size seq vrb outputs vv is the value of the ii ith element vv VALUE Value of an element in the sequence FIRST SEQ syntax vv FIRST SEQ preconditions the sequence must not be empty outputs vv is the value of the first element vv VALUE Returns the first element in the sequence LAST SEQ syntax vv LAST SEQ preconditions the sequence must not be empty outputs vv is the value of the last element vv VALUE Returns the last element in the sequence DESCRIPTION OF LIBRARY MACHINES 43 PUSH SEQ syntax PUSH SEQ vv preconditions vv must be in VALUE and the sequence must not be full Add vv at the end of the sequence POP SEQ syntax POP_SEQ preconditi
51. ge preconditions range must belong to the LSR minrge LSR maxrge range and the range position sequence cannot be empty Removes the first element in a sequence KEEP SEQ RGE syntax KEEP_SEQ_RGE range nn preconditions range must belong to the LSR_minrge LSR_maxrge range nn must be a NAT Only retains the nn first elements in a sequence For nn size seq_rge range this operation has no effect DESCRIPTION OF LIBRARY MACHINES 65 CUT_SEQ_RGE syntax CUT_SEQ_RGE range nn preconditions range must belong to the LSR_minrge LSR_maxrge range nn must be in NAT Clears the sequence of its first nn elements For nn size seq rge range this operation is equivalent to CLR_SEQ_RGE PART_SEQ_RGE syntax PART_SEQ_RGE range ii jj preconditions range must belong to the LSR_minrge LSR_maxrge range ii and jj must be NATs that are not null with ii lt jj In a sequence only retains the indexes between two limits ii jj may not be in the sequence domain REV SEQ RGE syntax REV_SEQ_RGE range preconditions range must belong to the LSR_minrge LSR_maxrge range Reverses the order of the elements in a sequence FIND_FIRST_SEQ_RGE syntax bb ii FIND FIRST SEQ RGE range vv preconditions range must belong t the LSR_minrge LSR_maxrge range vv must be in LSR VALUE outputs bb is TRUE if vv is in the range position sequence FALSE if not iiis a NAT if bb TRUE it indicates the first position
52. he index of this element is returned promoted operation SWAP_RGE swap two elements in a table promoted operation RIGHT_SHIFT_RGE shift a table range to the large index promoted operation LEFT_SHIFT_RGE shift a table range to the small index promoted operation SEARCH MAX EQL RGE search for the last element that equals a value in a table range promoted operation SEARCH MIN EQL RGE search for the first element that equals a value in a table range promoted operation REVERSE RGE reverses the order of the elements of a part of a table promoted operation SEARCH MIN GEQ RGE search for the first element that exceeds a value in a table range ASCENDING SORT RGE sort a table range into ascending order L SEQUENCE RANGE sequence range LEN_SEQ_RGE determines the length of a sequence IS FULL SEQ RGE determines whether a sequence is full IS INDEX SEQ RGE determines whether an integer is in a sequence range VAL SEQ RGE gives the value of a sequence for a valid index FIRST SEQ RGE gives the first element in a sequence LAST SEQ RGE gives the last element in a sequence PUSH SEQ RGE adds an element to a sequence POP SEQ RGE removes the last element from a sequence STR SEQ RGE changes the value of a sequence element RMV SEQ RGE removes an element from a sequence with a size that decreases by 1 INS_SEQ_RGE adds an element to a sequence with a size that increases by 1 CLR SEQ RGE clears a sequen
53. ible with the previous machine L ARRAY COLLECTION where index sets are normally unordered MACHINE PARAMETERS L ARRAYI COLLECTION LAUC_maxobj LAUC_maxidx LAUC_minval LAUC_maxval The variable is a partial function of 1 LAUC_maxobj in the set of to tal functions of 0 LAUC_maxidx to LAUC_minval LAUC_maxval LAUC_maxobj is a NATI that is different from MAXINT LAUC_maxidx LAUC_minval and LAUC_maxval are NATs and LAUC_minval lt LAUC_maxval CRE_ARR_COL Syntax ii bb CRE_ARR_COL Outputs bb is a Boolean element indicating whether any available arrays remain in the collection ii is the index of this available array Allocate an array in the collection DEL_ARR_COL Syntax DEL_ARR_COL ii Preconditions ii must belong to 1 LAUC maxobj Array ii in the collection is released It may once again be assigned using CRE ARR COL DESCRIPTION OF LIBRARY MACHINES 71 VAL_ARR_COL Syntax vv VAL ARR COL ii jj Preconditions ii must belong to 1 LAUC_maxobj jj must belong to 1 LAUC maxidx Output vv contains the value of number jj in array ii Store in vv the value of number jj in array ii STR ARR COL Syntax STR ARR COL ii jj vv Preconditions ii must belong to 1 LAUC_maxobj jj must belong to 1 LAUC maxidx vv must belong to LAUC VALUE Write value vv to the jjth cell in array ii COP ARR COL Syntax COP ARR COL dest src Preconditions dest and src must belong to 1 LAUC maxobj Copy the conte
54. ion for the logarithm and the square root return the best ap proaching value in NAT The used algorithms are optimized MACHINE PARAMETERS None The NAT element immediatly inferior or superior wether the calcul is performed by inferior value or superior value DESCRIPTION OF LIBRARY MACHINES 27 MIN syntax preconditions outputs MAX syntax preconditions outputs INC syntax preconditions outputs DEC syntax preconditions outputs EXP syntax preconditions outputs uu MIN vv ww vv and ww must be in NAT uu min vv ww uu MAX vv ww vv and ww must be in NAT uu receives max vv ww uu INC vv vv must be in 0 MAXINT 1 uu vv 1 uu DEC vv vv must be in 1 MAXINT uu vv 1 rr EXP xx nn xx and nn must be in NAT xx and nn must not both be nil xx must be less than or equal to MAXINT rr receives xx EXP returns xx to the power of nn Calculating 0 is illegal 0 is not defined The implementation uses a fast algorithm based on breaking down into base 2 of nn logo nn iterations SQRT syntax preconditions outputs nn SQRT pp pp must be in NAT nn so that nnxnn lt pp lt nn 1 x nn 1 SQRT returns the largest nn so that nnxnn lt pp The implementation uses an algo rithm that performs SQRT nn iterations where each iteration costs two additions and a subtraction LOG BY DEFAULT syntax preconditions out
55. l the indexes between ii to jj If ii gt jj the array does not change Note that it would not have been advisable to set ii lt jj as a precondition of this operation as this would have limited its use Let us consider the case of a call to SET ARRAY in a loop The last iteration fo the loop contain s a call with the form SET ARRAY ii jj vv with ii jj 1 The presence of a precondition in the definition of the operation SET_ARRAY would force us to guard all the calls to SET ARRAY by an IF More generally the precondition must be selected as minimal to protect us fromm a B code of defensive aspect IMPORTS REQUIRED None WARNING The implementation of this machine creates the default instance for the BASIC ARRAY VAR machine IMPORTS BASIC ARRAY VAR The addition of an instance of the machine BASIC ARRAY VAR requires choosing a new instance name as for example il BASIC ARRAY VAR Indeed the loops used make a pre incrementation that does not produce literal excedent DESCRIPTION OF LIBRARY MACHINES 31 5 3 L_ARRAY3 Array with Non Ordered Values Maximum Op erations OPERATIONS VAL ARRAY value of an element promoted operation STR ARRAY write an element promoted operation SET ARRAY write the same value in an array portion promoted operation SWAP ARRAY exchange two elements promoted operation RIGHT SHIFT ARRAY shift a portion to the main index promoted operation LEFT SHIFT ARRAY shift
56. low STRING WRITE syntax STRING_WRITE ss preconditions ss must be an element in the STRING set Will display a character string on screen For ss use quoted strings A C type formatting is used even for a translation into ADA i e t produces a tab E produces Escape B produces a sound produces a quote 22 Reusable Components Reference Manual KNOWN PROBLEMS STRING does not have a coherent definition The prover proves that any character string belongs to STRING due to an ad hocrule that does not derive from the definition STRING seq CHAR In addition using a STRING type local variable in an implementation is not possible To be completely rigorous nothing ensures that the operator performs all the requested entries Therefore the operations for entering the true data entry module BASIC IO c for example do not really implant the specifications of the corresponding B operations PROGRAMMING A more complete example IMPLEMENTATION bio_l REFINES bio IMPORTS BASIC_ARITHMETIC BASIC_IO OPERATIONS main VAR zz bb cc IN zz INTERVAL READ 0 100 STRING WRITE this is the value jr INT WRITE zz CHAR WRITE 10 per bb BOOL READ END lio STRING WRITE this is the value BOOL WRITE bb CHAR WRITE 10 cc CHAR READ STRING WRITE this is the value INT WRITE cc STRING WRITE CHAR WRITE cc CHAR WRITE 10 END END Exe
57. me siz 67 ARRAYI CO ON array of the same size with numerical indexes 69 OC Reusable Components Reference Manual INTRODUCTION 1 1 Introduction The reusable components supplied with Atelier B are basic machines and library machines Basic machines are the modelisation in B of modules manually coded in C C or ADA These modules are used to encapsulate the operating system functions that must be used they must usually be performed in taking into account the specificities of the hardware that the security software will run on This is why there are few basic machines delivered with Atelier B Library machines are abstract machines written in B language They generally model a type of mathematical object sequence function etc and offer the operations that allow the handling of these objects Unlike basic machines library machines are properly performed using the B method i e using refining and implementation in B along with complete proof of the set This proof may in principle be executed at any time in order to check its validity warning proving methods may depend on the demonstrator version used Therefore unlike basic machines library machines may be numerous and complex while remaining secure as they are proven To use basic machines simply reference them in the appropriate B project by INCLUDES IMPORTS or any derived actions When the final project is translated into a traditional prog
58. nce in their name For each mathematical object it is possible to realize either a variable representing the object or a variable representing several objects of this type For each type of object it is therefore possible to realize e The object itself e An array of objects with the same type same size these are machines with a name containing the RGE range radical e partial function of objects with the same size and same type these are machines with a name containing the COL collection radical e A partial function of objects with the same type but with various sizes OBJ radical The RGE and COL type machines produce objects that consume the memory neces sary for the maximum number of required objects For example if we create a range or a collection of three sequences of at least ten elements we will always require 30 memory spaces but the use of a collection avoids the user program to manage the sequences avail able occupied Object machines reserve a memory space that may be freely distributed depending on the created objects and their size Mathematical objects listed above are not all available on the different types of machines refer to library machines table of contents for the list that corresponds to the current version WARNING Most of the library machines are based on the basic machines BASIC ARRAY VAR and BASIC ARRAY RGE The manual implementations of the basic machines B
59. nents with the Ada C and C translators 2 Reusable Components Reference Manual supplied with Atelier B These translators are experimentals Their goal is to show that it is possible to translate some BO implementations into classical programming languages Therefore their use is not guaranteed Especially the reusable components use may induce errors when compiling the code produced by the translators The reusable components must be considered as examples Each user can develop his own library machines according to his needs INDEX OF BASIC MACHINES 3 2 Index of Basic Machines BASIC_ARRAY_VAR implanting a one dimension table VAL_ARRAY read a table element STR_ARRAY write a table element BASIC_ARRAY_RGE implementing a two dimensional table VAL_ARR_RGE read a table element STR_ ARR_RGE write a table element COP_ARR_RGE copy a table line to another CMP_ARR_RGE compare two table lines BASIC IO vt 100 style input output INTERVAL_READ entry by the operator of a number in mm nn INT_WRITE print a number BOOL_READ entry by a TRUE or FALSE boolean operator BOOL_WRITE print the TRUE or FALSE condition CHAR_READ entry by a character s operator CHAR WRITE print a character STRING WRITE print a message Reusable Components Reference Manual INDEX OF LIBRARY MACHINES 5 3 Index of Library Machines L_ARITHMETIC1 extended integer operations MIN MAX INC DEC EXP SQRT LOG VAL_ARR_RGE read a table elem
60. nt of a sequence PUSH SEQ RGE syntax PUSH_SEQ_RGE range vv preconditions range must belong to the LSR_minrge LSR_maxrge range vv must be in LSR_VALUE and the range position sequence cannot be full Adds an element to a sequence 64 Reusable Components Reference Manual POP SEQ RGE syntax POP SEQ RGE range preconditions range must belong to the LSR minrge LSR maxrge range the range position sequence must not be empty Removes the last element in a sequence STR SEQ RGE syntax STR_SEQ_RGE range ii vv preconditions range must belong to LSR_minrge LSR_maxrge ii be a valid index in the range position sequence and vv belong to LSR_VALUE Change the value of an element in a sequence RMV SEQ RGE syntax RMV_SEQ_RGE range ii preconditions range must belong to the LSR_minrge LSR_maxrge range ii must be a valid index in the range sequence Removes an element from a sequence the size of which decreases by 1 INS AFT SEQ RGE syntax INS AFT SEQ RGE range ii vv preconditions range must belong to the LSR minrge LSR maxrge range ii must be a valid index in the range position sequence vv must be in LS5R VALUE the range position sequence must not be full Adds an element to a sequence the size of which increases by 1 CLR SEQ RANGE syntax CLR_SEQ RANGE range preconditions range must belong to the LSR_minrge LSR_maxrge range Clears a sequence TAIL SEQ RGE syntax TAIL SEQ RGE ran
61. ntifies whether a number is a valid index VAL SET value of an element in the set EXAMPLE The example below shows the use of L SET on a listed set IMPLEMENTATION ml1 1 MACHINE REFINES i ml SETS IMPORTS ST cat dog bird VARIABLES T ELSOT e INVARIANT INVARIANT set vrb is the variable in L SET vv C ST ran set vrb vv INITIALISATION IEEE eon i L SET ensures that the set is empty at the start vv cat bird END INS_SET cat INS SET bird END DESCRIPTION L SET creates a set that is modeled by an injective sequence type variable set vrb the maximum size of which is a machine parameter It offers functions to search for add and delete elements The use of an injective sequence type variable enables easy access to each element of the set via an index The user can therefore create loops by using the CARD SET and VAL SET functions This would not have been possible if the variable directly represented the set WARNING The user must add the gluing invariant ran set vrb var locale to his machine in order to link his set variable with the L SET machine state 46 Reusable Components Reference Manual MACHINE PARAMETERS L_SET LSET maxsize LSET VALUE the variable is an injective sequence of elements from LSET VALUE with a maximum size LSET maxsize CARD SET syntax nn CARD SET output nn is the size of the set the cardinal of ran set vrb Therefore nn belongs to
62. nts of the src array to the dest array CMP ARR COL Syntax bb CMP ARR COL range 1 range 2 Preconditions range 1 and range 2 must belong to 1 LAUC maxobj Output bb is a Boolean element that indicates whether array ranges 1 and 2 are identical Comparison between the two arrays SET ARR COL Syntax SET ARR COL range ii jj vv Preconditions range belonging to dom arr col ie it corresponds to the index of a previously created array ii and jj are in 1 LAUC_maxidx jj must be different from MAXINT vv is in LAUC minval LAUC maxval The value vv is copied to the range array for all indexes between ii and jj If ii jj the array remains unchanged PCOP ARR COL Syntax PCOP ARR COL dest idx dst src ii jj Preconditions dest and src are elements that are different from 1 LAUC maxobj cor responding to arrays already created ii jj is a non blank interval of 0 LAUC maxidx and jj MAXINT idx dst idx dst jj ii is an interval of 0 LAUC_maxidx The ii jj part in the src array is copied to the idx dst idx dst jj ii part of the dst array 72 Reusable Components Reference Manual PCMP ARR COL Syntax idx bb PCMP_ARR_COL nn2 idx2 nnl ii jj Preconditions nnl and nn2 are elements that are different from 1 LAUC maxobj and correspond to arrays already created ii jj is a non blank interval of 0 LAUC maxidx idx2 idx2 jj ii is an interval of 0 LAUC maxidx Outputs bb
63. of part ii jj from the array shift nn spaces to the left DESCRIPTION OF LIBRARY MACHINES 33 SEARCH MAX EQL ARRAY syntax rr bb SEARCH_MAX_EQL_ARRAY ii jj vv preconditions ii and jj must be in 0 LAT_maxidx ii jj and vv belong to LAT VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the largest index in the array worth vv Search for an array element equal to vv by scanning the ii jj part starting from jj SEARCH MIN EQL ARRAY syntax rr bb SEARCH_MIN_EQL_ARRAY ii jj vv preconditions ii and jj must be in 0 LAT_maxidx ii jj and vv belong to LAT VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the smallest index in the array worth vv Search for an array element that equals vv by scanning the ii jj part starting from ii REVERSE ARRAY syntax REVERSE ARRAY ii jj preconditions ii and jj must be in 0 LAT maxidx Reverse the order of elements in the ii jj portion of the array IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the default instance for the BASIC ARRAY VAR machine clause IMPORTS BASIC ARRAY VAR Therefore if another instance is necessary it must be given a different instance name for example il BASIC ARRAY VAR 34 Reusable Components Referen
64. onditions rng must belong to LACR_minrge LACR_maxrge ii and jj belong to 0 LACR maxidx ii lt jj and vv must belong to LACR VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr the largest index in the array that equals vv Search for an array element that equals vv by scanning the ii jj part starting from jj SEARCH MIN EQL RGE syntax rr bb SEARCH MIN EQL RGE rng ii jj vv preconditions rng must belong to LACR_minrge LACR_maxrge ii and jj belong to 0 LACR maxidx ii lt jj and vv must belong to VALUE outputs TRUE if vv was found FALSE if not rr is a NAT if bb TRUE then rr is the smallest index in the rng array equal to vv Search for an element in an array equal to vv by scanning the ii jj part starting from ii REVERSE RGE syntax REVERSE RGE rngji jj preconditions rng must belong to LACR_minrge LACR_maxrge ii and jj belong to 0 LACR maxidx Reverse the order of elements in the ii jj range of the rng array 60 Reusable Components Reference Manual SEARCH MIN GEQ RGE syntax ii bb SEARCH_MIN_GEQ_RGE rng jj kk vv preconditions rng must belong to LACR_minrge LACR_maxrge jj and kk belong to 0 LACR_maxidx jj lt kk and vv belong to LACR_minval LACR_maxval For implementation reasons kk must be different from MAXINT outputs bb is a Boolean element TRUE is an element that exceeds or is equal to the vv value found FALSE if not ii is a NAT if bb TR
65. ons the sequence must not be empty Removes the last element from the sequence its value is lost STR_SEQ syntax STR_SEQ ii vv preconditions vv must be in VALUE and ii must be a valid index for the sequence Changes the value of an existing element in the sequence RMV_SEQ syntax RMV_SEQ ii preconditions ii must be a valid index in the sequence Removes an element from the middle of the sequence INS_AFT_SEQ syntax INS AFT SEQ ii vv preconditions vv must be in VALUE and ii must be a valid index for the sequence The sequence must not be full Inserts vv right after index ii CLR SEQ syntax CLR SEQ Clears the sequence TAIL SEQ syntax TAIL_SEQ preconditions the sequence must not be empty Removes the first element from the sequence KEEP_SEQ syntax KEEP_SEQ nn preconditions nn must be a NAT Only retains the nn first elements in the sequence For nn size seq vrb this operation does not take action 44 Reusable Components Reference Manual CUT_SEQ syntax CUT_SEQ nn preconditions nn must be a NAT Deletes the nn first elements from the sequence For nn size seq_vrb this operation is equivalent to CLR_SEQ PART_SEQ syntax PART_SEQ ii jj preconditions ii and jj must be non null NATs with ii lt jj Only retains the ii jj portion in the sequence ii jj may not be included in the domain of the sequence REV_SEQ syntax REV_SEQ Reverses the order of the elements in the sequence Applies
66. operation implanted using a shift sort fast algorithm DESCRIPTION OF LIBRARY MACHINES 35 MACHINE PARAMETERS L_ARRAY5 LAC_minval LAC_maxval LAC_maxidx LAC_minval LAC_maxval is the set of possible values for the elements in the array 0 LAC_maxidx is the set of index values for the array LAC_minval LAC maxval LAC maxidx must be NATs this machine does not allow negative values It is also necessary for LAC minval xLAC maxval and 1 lt LAC_maxidx VAL_ARRAY syntax vv VAL_ARRAY ii preconditions ii must be in 0 LAC_maxidx outputs vv is in LAC_minval LAC_maxval is the array value at position ii STR_ARRAY syntax STR ARRAY ii vv preconditions ii must be in 0 LAC_maxidx and vv in LAC_minval LAC_maxval and LAC VALUE The vv value is stored in the array at index ii SET ARRAY syntax SET_ARRAY ii jj vv preconditions ii jj must be included in 0 LAC maxidx and vv must bein LAC VALUE For implementation it is also necessary that jj be different from the MAXINT constant The vv value is stored in the array for all indexes from ii to jj If ii gt jj the array does not change SWAP_ARRAY syntax SWAP_ARRAY ii jj preconditions iijj must be in 0 LAC_maxidx The ii and jj elements in the array are exchanged RIGHT_SHIFT_ARRAY syntax RIGHT SHIFT ARRAY ii jj nn preconditions iijj onn must be in 0 LAC_maxidx with ii lt jj and jj nn lt LAC_maxidx to make possible the right shift by nn sp
67. puts uu rr LOG BY DEFAULT vv ww ww and vv are two natural integers and vv is between 2 and MAXINT uu is the smallest natural so that vv is strictly greater than ww By definition uu is a natural integer rr takes the value vv 28 Reusable Components Reference Manual LOG BY DEFAULT in base vv of ww returns the smallest uu value so that ww vv c This gives vv ww except if ww lt vv example ww 0 Does not work for vv 0 or 1 as 0 and 1 are constants rr receives the value of vv which easily allows judging the error made LOG BY EXCESS syntax uu bb LOG BY EXCESS vv ww preconditions ww belongs to NAT and vv is an element of the intervall 2 MAXINT outputs uu receives the smallest natural so that vv is greater than or equal to ww uu must be in NAT bb is an element of BOOL it indicates whether the logarithm is an exact one LOG BY EXCESS in base vv in ww returns the smallest uu so that wwxvv WARN ING vv may exceed MAXINT Does not work for vv 0 or 1 as 0 and 1 are constants bb equals TRUE if ww vv IMPORTS REQUIRED None DESCRIPTION OF LIBRARY MACHINES 29 5 2 L_ARRAY1 One Dimensional Array with Initialization Loop OPERATIONS VAL ARRAY value of an element promoted operation STR ARRAY write an element promoted operation SET_ARRAY write the same value in a portion of the array EXAMPLE Use SET_ARRAY to initialize an array IM
68. ramming language the translation of the library machine implementations used must be redone if this was not already done at Atelier B installation Library machines are implemented on basic machines As they are performed until the implementation in B language they provide complete examples of use in the B method They especially contain examples of proven WHILE loops For practical advice on proving WHILE loops refer to the B Language User Manual The user may directly use library machines just like he uses basic machines Sometimes the implementation of a library machine may use the services of a machine that it does not create an instance for use by SEES to avoid duplications In this case the user will have to create the instance in question using IMPORTS by following the indications in the IMPORTS REQUIRED section of the description for each library machine When the final project C C or ADA compilation is performed the library compilation is automatically performed if necessary Performing link editing will then enable incor poration into the final executable program only those object files that correspond to the library machines actually used All this is performed in the Makefile produced by Atelier B To integrate a software component produced by Atelier B into a traditional product use this Makefile as a basis or refer to the ADA Translator User Manual Warning This warning regards the use of reusable compo
69. that equals vv in the sequence Searches for a value in a sequence starting from the beginning FIND LAST SEQ RGE syntax bb ii FIND LAST SEQ RGE range vv preconditions range must belong to the LSR_minrge LSR_maxrge range vv must be in LSR VALUE outputs bb is TRUE if vv is in the range position sequence FALSE if not ii is a NAT if bb TRUE this indicates the last position that equals vv in the sequence Searches for a value in a sequence starting from the end COP SEQ RGE syntax COP_SEQ_RGE dst src preconditions dst and src must belong to the LSR_minrge LSR_maxrge range Copy the seq_rge src sequence to the seq_rge dst sequence 66 Reusable Components Reference Manual CMP_SEQ RGE syntax bb CMP_SEQ_RGE rngl rng2 preconditions rngl and rng2 must belong to the LSR minrge LSR maxrge range outputs bb is TRUE if the two rng1 and rng2 position sequences are equal FALSE if not Compare two sequences PCOP SEQ RGE syntax PCOP_SEQ_RGE dst idx src ii jj preconditions dst and src must belong to the LSR_minrge LSR_maxrge range dst must be different from src ii and jj must be valid indexes in the src position sequence with ii lt jj and jj MAXINT 1 idx must be a valid index for the dst sequence or where the size of this sequence 1 idx jj ii belongs to the 1 LSR_maxsize range Copy the ii jj part of the src position sequence to the dst position from the idx index
70. the array line rr index ii COP ARR RGE syntax COP_ARR_RGE dest src preconditions dest and src must be elements of BAR RANGE The src line is copied to the dest line CMP ARR RGE syntax bb CMP_ARR_RGE rangel range2 preconditions rangel and range2 must be elements of BAR RANGE outputs bb is an element of BOOL that takes the TRUE value if the two lines are equal C LANGUAGE In C the array is realised by an array of pointers pointing on integers arrays The access to these arrays are done using methods that refuse the index used between 0 and the arrays size guaranting an optimal memory occupation The memory is dynamically reserved when lauching the program If the size indicated by the formal parameters is too big the program stops with the following message Virtual memory exceeded in new DESCRIPTION OF BASIC MACHINES 19 C LANGUAGE The realisation in C is based on the same principles as in C The stop message on the Fatal error Malloc of X bytes failed initial reservation failure is i Execution of current application is aborted ADA LANGUAGE The use of generic packages guarantees an optimal memory occupation No restriction is made on the instancing parameters On an initial reservation failure an exception stops the program 20 Reusable Components Reference Manual 4 3 BASIC IO vt100 style inputs outputs OPERATIONS INTERVAL READ operator input of an integer in mm nn
71. well as LPF_maxval lt MAXINT This is because MAXINT is used to indicate that the corresponding index is not part of the partial function Again to simplify implementation it is also illegal to have LPF_maxidx MAXINT VAL_PFNC syntax vv VAL_PFNC ii preconditions ii must be in the partial function domain outputs vv is in LPF_minval LPF_maxval it is the value of the array at position ii STR_PFNC syntax STR_PFNC ii vv preconditions ii must be in 0 LPF_maxidx and vv be in LPF_minval LPF_maxval The partial function is overloaded by ii vv XST_PFNC syntax bb XST_PFNC ii outputs bb is TRUE if ii is in the domain of the function FALSE if not RMV_PFNC syntax RMV PFNC ii preconditions ii must be in the domain of the partial function The ii pfnc vrb ii pair is removed from the partial function pfnc vrb SET PFNC syntax SET_PFNC ii jj vv preconditions ii jj must be included in 0 LPF_maxidx and vv be in LPF_minval LPF _maxval ii and jj must be NATs The partial function is overloaded by ii jj x vv If ii jj ii jj is blank and the partial function is not modified but it is still necessary for ii and jj to be NATs SWAP PFNC syntax SWAP_PFNC ii jj preconditions iijj must be in the domain of the partial function The ii and jj elements in the array are exchanged DESCRIPTION OF LIBRARY MACHINES 39 RIGHT_SHIFT_PFNC syntax RIGHT_SHIFT_PFNC ii jj nn preconditions iijj onn must
72. xrge For implementa tion reasons dest2 must also be different from MAXINT The src array is duplicated in all of the arrays of the dest1 dest2 interval 50 Reusable Components Reference Manual PCOP_ARR_RGE syntax PCOP_ARR_RGE dest idx_dst src ii jj preconditions dest and src must be different elements of LAUR minrge LAUR maxrge ii jj be a non empty interval of 0 LAUR_maxidx idx dst belong to 0 LAUR_maxidx jj be different from MAXINT and idx_dst jj ii belong to 0 LAUR_maxidx condition necessary to ensure that the copy does not overflow The ii jj part of the src array is copied to the dest array from the idx_dst index PCMP_ARR_RGE syntax idx bb PCMP_ARR_RGE rng2 idx2 rng1 ii jj preconditions rngl and rng2 must belong to LAUR_minrge LAUR_maxrge ii jj be a non empty interval of 0 LAUR_maxidx idx2 and idx2 jj ii are in 0 LAUR maxidx The ii jj part of array rng is compared to the part with the same size in the rng2 array The idx2 jj ii 0 LAUR maxidx condition guarantees that this comparison is possible bb is a Boolean element that is FALSE if the two parts are equal and TRUE if they are different In the latter case idx and index are the first element that is different from ii jj IMPORTS REQUIRED instances to import as the implementation tree for this library machine sees them with SEES BASIC ARITHMETIC BASIC BOOL WARNING The implementation of this machine creates the de
73. y part of one of the arrays to a different array to a given position promoted operation PCMP_ARR_RGE search for the first different element between two parts of two ar rays A Boolean element indicates whether this element was found and in this case the index of this element is returned promoted operation SWAP RGE exchange two elements in an array promoted operation RIGHT SHIFT RGE shift a part of an array to the large index promoted operation LEFT_SHIFT_RGE shift a part of an array to the small index promoted operation SEARCH MAX EQL RGE search for the last element that is equal to a value in an array range promoted operation SEARCH MIN EQL RGE search for the fist element that equals a value in an array range promoted operation REVERSE RGE reverse the order of the elements of a part of an array promoted operation SEARCH MIN GEQ RGE search for the first element that exceeds a value in an array range ASCENDING SORT RGE sort part of an array and arrange in ascending order DESCRIPTION OF LIBRARY MACHINES 57 EXAMPLE IMPLEMENTATION m5_1 er cna REFINES m5 ee iMmponre INVARIANT a MEM vv 0 20 0 4 0 255 arr rge vv V xx yy xx 0 20 yy 0 3 INITIALISATION gt vwv yy xx gt vv yy xx 1 INITIALISATION vv vv 0 20 0 4 0 255 V xx yy xx 0 20 A yy 0 3 gt SET ARR RGE 0 0 4 50 STR ARR RGE 0 2 10 STR ARR RGE 0 4 30 ASCEN

reusable_components_..

Contents

Download Pdf Manuals

Related Search

Related Contents