| Abstraction |
Shape-value abstraction of assertions
|
| Actions |
Rely-guarantee actions
|
| Assertions |
Separation logic assertions (symbolic heaps)
|
| Commands |
Representation of program commands
|
| Convert |
Translate parse tree into the intermediate abstract syntax tree
|
| Exp |
Representation of expressions
|
| Genarith |
Generation of arithmetic programs
|
| Indpreds |
User-defined inductive predicates
|
| Linear |
Linearizability
|
| Location |
Source file locations (for error messages)
|
| Lockfree |
Lock-freedom prover
|
| Misc |
Library functions and miscellaneous routines
|
| Parsetree |
Abstract syntax tree produced by the parser
|
| Prover |
Must-subtraction implementation
|
| Pure |
Operations on pure formulae
|
| Symbsimp |
Symbolic execution
|
| Tycheck |
Type checking & conversion into command language
|