Documentation
Input format
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))
...