-
Notifications
You must be signed in to change notification settings - Fork 0
/
BASIC_ARRAY_VAR.mch
43 lines (36 loc) · 954 Bytes
/
BASIC_ARRAY_VAR.mch
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
/******************************* CLEARSY *************************************
* File : $Id: $
* (C) 1998 CLEARSY
*
* Description : BASIC_ARRAY_VAR : modelisation for one dimensionnal
* total functions
*
*
* History : $Log: $
*
******************************************************************************/
MACHINE
BASIC_ARRAY_VAR(BAV_INDEX,BAV_VALUE)
VARIABLES
arr_vrb
INVARIANT
/*----------------------------------------------------------------------**
arr_vrb is a total function from BAV_INDEX towards BAV_VALUE, that describes
an array.
**----------------------------------------------------------------------*/
arr_vrb: BAV_INDEX --> BAV_VALUE
INITIALISATION
arr_vrb:: BAV_INDEX --> BAV_VALUE
OPERATIONS
vv <-- VAL_ARRAY(ii) = PRE
ii: BAV_INDEX
THEN
vv:=arr_vrb(ii)
END;
STR_ARRAY(ii,vv) = PRE
ii: BAV_INDEX &
vv: BAV_VALUE
THEN
arr_vrb(ii):=vv
END
END