A | |
| Abstraction |
Shape-value abstraction of assertions
|
| Actions |
Rely-guarantee actions
|
| Assertions |
Separation logic assertions (symbolic heaps)
|
C | |
| Commands |
Representation of program commands
|
| CompSet [Misc] | |
| Convert |
Translate parse tree into the intermediate abstract syntax tree
|
D | |
| Dset [Exp] |
Disjoint sets
|
E | |
| E [Exp] | |
| Exp |
Representation of expressions
|
F | |
| Fld [Exp] | |
G | |
| Genarith |
Generation of arithmetic programs
|
I | |
| Id [Exp] |
Identifiers
|
| IdMap [Exp] | |
| IdSet [Exp] | |
| Indpreds |
User-defined inductive predicates
|
L | |
| Linear |
Linearizability
|
| List [Misc] |
Operations on linked lists
|
| Location |
Source file locations (for error messages)
|
| Lockfree |
Lock-freedom prover
|
M | |
| Misc |
Library functions and miscellaneous routines
|
P | |
| PList [Misc] |
Packed association lists
|
| Parsetree |
Abstract syntax tree produced by the parser
|
| Prover |
Must-subtraction implementation
|
| Pure |
Operations on pure formulae
|
S | |
| StringMap [Misc] | |
| StringSet [Misc] | |
| Symbsimp |
Symbolic execution
|
T | |
| Tycheck |
Type checking & conversion into command language
|