| | 2 | |
| | 3 | == The CIVL-C Language == |
| | 4 | |
| | 5 | Under construction. |
| | 6 | |
| | 7 | * [wiki:CIVL-C Overview] |
| | 8 | * structure of a CIVL-C program, top-level elements, translation to a model |
| | 9 | * [wiki:Types] |
| | 10 | * discussion of types and their domains without syntax: primitive types, record types, scope type, proc type, pointer types, scope-parameterized pointer types, array types |
| | 11 | * domain of pointer types: variable references, array element references, record member reference |
| | 12 | * [wiki:Declarations] |
| | 13 | * variable and procedure declarations, procedure definitions, scope declarations, type definitions, scope-parameterized declarations, first-class array type decls |
| | 14 | * declarations of system procedures, `$pure` procedures, procedure contracts |
| | 15 | * [wiki:Expressions] |
| | 16 | * usual operations, array operations |
| | 17 | * [wiki:Statements] |
| | 18 | * `$spawn`, `$wait`, `$assume`, ... |
