The input format of the VVT is based on the SMTLib2-format. The format describes the transition relation of the program as an extended logical circuit. The basic structure of a program consists of
- A state vector describing the types of the state variables
- An input vector which contains nondeterministic variables
- Definitions of gates
- The definition of the next state
- The definition of the initial state
- Properties that should be verified
(program (state ...) (input ...) (gates ...) (next ...) (init ...) (property ...) )
The state vector is a list of pairs of variable names and types. For example, if your program has an integer named “x” and a boolean called “c”, the state vector would look like this:
... (state (x Int) (c Bool)) ...
The input vector has the same format as the state vector. For example, a program with a boolean input variable “y” would have the input vector:
... (input (y Bool)) ...
Gates allow you to bind expressions to names to avoid repetition of common expressions. For example, if you wanted to use the expression “x+x” more than once, you could bind it to the name “twox” like so:
... (gates (twox Int (+ x x))) ...
To specify how the successor state is defined, we add a definition for every state variable in the “next” list:
... (next (x (ite c twox x)) (c (and c y))) ...
The starting state of the program is specified using the “init” list:
... (init (x 0) (c True)) ...
Properties that should be verified by either vvt-verify or vvt-bmc can be specified in the list of properties. For example, to specify that “x” is always smaller than 100, we can say:
... (property (< x 100)) ...