Logic
Booleans
Like many languages, Vehicle has 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 |
|
|
|
Disjunction |
|
|
|
Implication |
|
|
|
Negation |
|
|
|
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.
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.
Note
Due to decidability and query dependency issues, the condition of an
if then else
statement may not contain a quantification over
a variable with an infinite domain. For example, the following is not allowed:
if (forall (x : Rat) . f x > 0) then 2 else 3
Equality
Two expressions of the same type can be tested for equality/inequality
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 ofd
.List A
if typeA
also supports the operators.Vector A n
if typeA
also supports the operators.Tensor A dims
if typeA
also supports the operators.
For example:
forall x . x != 0 => f x == 1