# Properties

## Basics

A property is any self-contained statement that you wish to check using Vehicle.
Properties are declared by annotating declarations with the `@property`

annotation:

```
@property
robust : Bool
robust = forall x . f x ! 0 >= 0.0
```

Only declarations with the types `Bool`

, `Vector Bool n`

or `Tensor Bool n`

may
be annotated as properties. In the latter case, Vehicle will report the status of each
element of the `Vector`

or `Tensor`

individually.

## The `foreach`

quantifier

A common use of the `forall`

quantifier is to assert that a
predicate holds over every element of a dataset, e.g.

```
@dataset
trainingDataset : List (Tensor Rat [28, 28])
...
robust : Bool
robust = forall x in trainingDataset . robustAround x
```

The problem with this formulation of the specification is that Vehicle
will only report whether the network is robust around *all* the elements
in the dataset. This is unlikely to be true.

Instead the `foreach`

quantifier may be used. Instead of returning a
single value of type `Bool`

it constructs a `Tensor`

of `Bool`

values. When used a property, Vehicle will therefore report
on the verification status of each individual element.

```
@dataset
trainingDataset : List (Tensor Rat [28, 28])
...
robust : List Bool
robust = foreach x in trainingDataset . robustAround x
```

Unlike the `forall`

keyword, the `foreach`

keyword cannot be used to
quantify over infinite types. It _can_ be used to quantify over `Index`

types.