| 1 | Need to add:
|
|---|
| 2 | self
|
|---|
| 3 | true
|
|---|
| 4 | false
|
|---|
| 5 | result
|
|---|
| 6 | contracts: ensures requires: part of function decl
|
|---|
| 7 |
|
|---|
| 8 | ABC: front end for C
|
|---|
| 9 | ast: this will have library functions and state like
|
|---|
| 10 | MPI_Send, blah blah blah
|
|---|
| 11 |
|
|---|
| 12 | SARL: symbolic algebra and reasoning library
|
|---|
| 13 | provides representation, manipulation of symbolic expressions
|
|---|
| 14 | interface to theorem provers, etc.
|
|---|
| 15 |
|
|---|
| 16 | GMC: generic model checker
|
|---|
| 17 | provides depth first search, printing traces, ...
|
|---|
| 18 |
|
|---|
| 19 | CIVL: Concurrency Intermeidate Verification Language
|
|---|
| 20 | ast: similar to ABC AST but simpler
|
|---|
| 21 | uses: (nothing)
|
|---|
| 22 | provides: AST
|
|---|
| 23 | notes: no type qualifiers or other complicated C stuff.
|
|---|
| 24 | functions can be defined in any scope
|
|---|
| 25 | eventually add pointer scope qualifiers, etc.
|
|---|
| 26 | provide a side-effect remover and ASTMerger (like a linker, for libraries)
|
|---|
| 27 |
|
|---|
| 28 | front: common interface for all CIVL front-ends
|
|---|
| 29 | uses: ast
|
|---|
| 30 | provides: FrontEnd
|
|---|
| 31 | notes: provides methods to parse a file and produce an AST
|
|---|
| 32 |
|
|---|
| 33 | civlc: grammar and parser for CIVL-C language
|
|---|
| 34 | uses: front, ast
|
|---|
| 35 | provides: CivlCFrontEnd
|
|---|
| 36 | notes: the grammar of the CIVL-C language should be very
|
|---|
| 37 | closely aligned with the CIVL AST.
|
|---|
| 38 | this module is like ABC, but results in a CIVL AST.
|
|---|
| 39 | also uses library files in lib
|
|---|
| 40 | could this use the AST preprocessor?
|
|---|
| 41 |
|
|---|
| 42 | lib: libraries written in CIVL-C: mp.civl, etc.
|
|---|
| 43 | how is state and definitions incorporated into the module?
|
|---|
| 44 | notes: this is not java source, just CIVL-C source
|
|---|
| 45 |
|
|---|
| 46 | c: translator from C code to CIVL AST
|
|---|
| 47 | uses: ABC, ast, front, civlc
|
|---|
| 48 | uses ABC to create ABC-AST, then translated that to CIVL-AST
|
|---|
| 49 | needs to translate library calls to CIVL libraries, e.g.,
|
|---|
| 50 | MPI_Send -> CIVL_MP_send, etc. Hence needs to civlc
|
|---|
| 51 | to parse and construct library modules, then merge them
|
|---|
| 52 | needs to introduce scopes for MPI processes etc
|
|---|
| 53 |
|
|---|
| 54 | model: representation of a CIVL model, like in CVT
|
|---|
| 55 | uses: ast
|
|---|
| 56 | provides: Model, ModelBuilder
|
|---|
| 57 | notes: ModelBuilder translates AST to Model
|
|---|
| 58 | Model elements maintain back-pointers to AST nodes
|
|---|
| 59 |
|
|---|
| 60 | translates AST to Model
|
|---|
| 61 |
|
|---|
| 62 | state: representation and manipulation of states of a Model
|
|---|
| 63 | note: like CVT, but no buffers
|
|---|
| 64 |
|
|---|
| 65 | transition:
|
|---|
| 66 |
|
|---|
| 67 | predicate:
|
|---|
| 68 |
|
|---|
| 69 | kripke:
|
|---|
| 70 |
|
|---|
