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:

Cases-Statement with Match Expressions

Call to Proof Commands/Scripts

Repeat Statement

foreach/theonly Statement