This proof scripting language is suitable for interactive program verification.
The following types are supported:
- integer
- boolean
- strings
- logical terms (with type information in the future):
- int[]
- object
- field
- heap
- null
- formula
- any (top-type)
It supports the following language statements: