Logic

Booleans

Like many systems Vehicle contains booleans. The type of boolean values is Bool, and there are two values True and False.

The available operations over booleans are:

Operation	Symbol	Type	Example
Conjunction	and	Bool -> Bool -> Bool	x and y
Disjunction	or	Bool -> Bool -> Bool	x or y
Implication	=>	Bool -> Bool -> Bool	x => y
Negation	not	Bool -> Bool	not x

Conditionals

Conditional statements are written using the syntax if .. then .. else .. and have type Bool -> A -> A -> A for any type A. For example:

if f x > 0 then x < 0 else x > 0

In a functional language like Vehicle (and unlike in imperative languages) all statements must return a value. Therefore it is not possible to omit the else branch when writing a conditional.

Due to decidability issues, specifications that will be exported to a theorem prover may not contain if then else statements whose condition involves quantification over a variable with an infinite domain. For example, the following is not allowed:

if (forall x. f x > 0) then 2 else 3

Note

As discussed in the Tips and Tricks section, if then else should be used sparingly, as each conditional in the final normalised expression approximately doubles the time taken to verify the specification.

Equality

Two expressions of the same type can be declared to be equal or not equal using the == and != operators respectively.

The type of these operators are A -> A -> Bool where A can be any of the following types:

• Bool, Nat, Int, Rat.

• Index d for any value of d.

• List A if type A also supports the operators.

• Tensor A dims if type A also supports the operators.

For example:

forall x . x != 0 => f x == 1