# Compile-Time Verification and I/O

A surprisingly common question people ask me when I talk about compile-time checking of pre-/post-conditions and invariants is: how do you deal with I/O?

To understand what the difficulty is, let’s consider a simple example in Whiley:

```define nat as int where \$ >= 0
define pos as int where \$ > 0

define Rectangle as { nat x, nat y, pos width, pos height }
```

Here, we’ve defined a simple `Rectangle` data type which (intuitively) lives in a 2D space.  For whatever reason, the invariants on this data type restrict it’s `x` and `y` position to being non-negative, whilst the `width` and `height` must be at least `1` (i.e. zero-sized rectangles are not allowed).

Now the question: how do I read in a Rectangle from an I/O device (e.g. from the network)?  This is a fair question since we must assume that I/O devices are “untrusted”.  That is, we can read something which looks like a `Rectangle` from an I/O device, but we have no guarantee that the required Rectangle invariants are upheld.  This seems like a problem.

Let’s consider first a broken approach. This makes use of a method `::readInt()` for reading an integer from an `InputStream`:

```Rectangle readRectangle(InputStream in):
return {
x: x,
y: y,
width: w,
height: h
}
```

This program would generate a compile-time error in Whiley, because the verifier cannot prove the required `Rectangle` invariants are met by the value returned.  For example, it knows only that variable `w` is an `int` of some sort and, hence, that it could hold any valid integer value. Therefore, it cannot prove that `w > 0` holds which is required by the `Rectangle` invariant.

At this point, the answer is fairly straightforward: we need to check the data we’ve read matches the required invariants and, if not, report an error:

```Rectangle readRectangle(InputStream in) throws Error:
Now the verifier can now be certain that the required `Rectangle` invariants are met by the value returned. Whilst this idea is not exactly rocket science, it surprises me how often people miss it.