]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | /* |
e26e911c | 2 | ** A global attribute is not assosicated with a reference, but rather the |
80ee600a | 3 | ** global state of an execution. |
4 | ** | |
5 | ** Annotations are used in pre and post conditions (requires/ensures | |
6 | ** clauses). | |
7 | ** | |
8 | */ | |
9 | ||
e26e911c | 10 | global attribute sockets |
80ee600a | 11 | oneof uninitialized, initialized |
12 | annotations | |
13 | sockets_initialized clause ==> initialized | |
14 | sockets_uninitialized clause ==> uninitialized | |
15 | preconditions | |
16 | initialized as uninitialized ==> error | |
17 | "Uninitialized sockets do not satisfy precondition." | |
18 | postconditions | |
19 | initialized as uninitialized ==> error | |
20 | "Sockets initialized, but postcondition requires uninitialized sockets." | |
21 | merge | |
22 | initialized + uninitialized ==> error | |
23 | "Sockets initialized on true branch, uninitialized on false branch." | |
24 | uninitialized + initialized ==> error | |
25 | "Sockets uninitialized on false branch, initialized on true branch." | |
26 | default | |
27 | uninitialized | |
28 | end | |
29 | ||
30 | ||
31 |