|
This proof scripting language is suitable for interactive program verification. |
|
This proof scripting language is suitable for interactive program verification.
|
|
\ No newline at end of file |
|
|
|
|
|
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:
|
|
|
|
|
|
|
|
# Cases-Statement with Match Expressions
|
|
|
|
|
|
|
|
# Call to Proof Commands/Scripts
|
|
|
|
|
|
|
|
# Repeat Statement
|
|
|
|
|
|
|
|
# foreach/theonly Statement
|
|
|
|
|
|
|
|
|