| 10 | | == Sequential contracts == |
| | 10 | Note that the first three are also called function contracts, while the last is called loop contract. |
| | 11 | |
| | 12 | Additional primitives that extend ACSL include: |
| | 13 | * contract primitives for MPI |
| | 14 | * MPI collective contract |
| | 15 | * remote expressions |
| | 16 | * contract primitives for dependency relation |
| | 17 | * `depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis |
| | 18 | * `\calls(fun, arg0, arg1, ...)`: a set of actions that invokes the function with the specified arguments |
| | 19 | * `\noact`: empty set of actions |
| | 20 | * `\anyact`: any action sets |
| | 21 | * set of memory actions: `\read(mu-list)`, `\write(mu-list)` |
| | 22 | * action set operations: `+` union, `-` complement, `&` intersect |
| | 23 | * `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause |
| | 24 | * malicious primitives |
| | 25 | * wildcard term: `...` |
| | 26 | * additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope is used |
| | 27 | * extension for range with steps: `lo .. hi # step` |
| | 28 | |
| | 29 | The contract grammar could be found bellow: |
| | 30 | |
| | 31 | {{{ |
| | 32 | function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause? |
| | 33 | simple-clause∗ named-behavior∗ completeness-clause∗ |
| | 34 | requires-clause ::= requires pred ; |
| | 35 | terminates-clause ::= terminates pred ; |
| | 36 | decreases-clause ::= decreases term (for id)? ; |
| | 37 | guards-clause ::= guards pred ; |
| | 38 | simple-clause ::= assigns-clause | ensures-clause |
| | 39 | | allocation-clause | abrupt-clause-fn |
| | 40 | | reads-clause | depends-clause |
| | 41 | assigns-clause ::= assigns tsets ; |
| | 42 | tsets ::= location (, location) ∗ |
| | 43 | ensures-clause ::= ensures pred ; |
| | 44 | allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ; |
| | 45 | reads-clause ::= reads tsets; |
| | 46 | depends-clause := depends event (, event)*; |
| | 47 | named-behavior ::= behavior id : behavior-body |
| | 48 | behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗ |
| | 49 | assumes-clause ::= assumes pred ; |
| | 50 | completeness-clause ::= complete behaviors (id (, id)∗)? ; |
| | 51 | | disjoint behaviors (id (, id)∗)? ; |
| | 52 | term ::= \old ( term ) | \result | \nothing | ... |
| | 53 | pred ::= \old ( pred ) |
| | 54 | }}} |
| | 55 | |
| | 56 | {{{ |
| | 57 | tset ::= \empty |
| | 58 | | tset -> id |
| | 59 | | tset . id * tset |
| | 60 | | & tset |
| | 61 | | tset [ tset ] |
| | 62 | | term? .. term? |
| | 63 | | \union ( tset (, tset)∗ ) |
| | 64 | | \inter ( tset (, tset)∗ ) |
| | 65 | | tset + tset |
| | 66 | | ( tset ) |
| | 67 | | { tset | binders (; pred)? } |
| | 68 | | { term } term |
| | 69 | }}} |
| | 70 | |
| | 71 | {{{ |
| | 72 | literal ::= \true | \false | integer | real | string | character |
| | 73 | }}} |
| | 74 | |
| | 75 | {{{ |
| | 76 | bin-op ::= + | - | * | / | % | << | >> |
| | 77 | | == | != | <= | >= | > | < |
| | 78 | | && | || | ^^ |
| | 79 | | & | | | --> | <--> | ^ |
| | 80 | }}} |
| | 81 | |
| | 82 | {{{ |
| | 83 | unary-op ::= + | - | ! | ~ | * | & |
| | 84 | }}} |
| | 85 | |
| | 86 | {{{ |
| | 87 | term ::= literal | id | unary-op term | term bin-op term | term [ term ] |
| | 88 | | { term \with [ term ] = term } |
| | 89 | | term . id |
| | 90 | | {term \with.id =term } |
| | 91 | | term -> id |
| | 92 | | ( type-expr ) term |
| | 93 | | id ( term (, term)∗ ) |
| | 94 | | (term) |
| | 95 | | term ? term : term |
| | 96 | | \let id = term ; term sizeof ( term ) |
| | 97 | | sizeof ( C-type-name ) |
| | 98 | | id : term |
| | 99 | | string : term |
| | 100 | }}} |
| | 101 | |
| | 102 | |
| | 103 | == Contracts for Sequential Programs == |
