Unclear semantics for environment variables in the invariant block

The semantics of invariants that refer to environment variables are currently very unclear. For example, does the following mean "`value` is always set to the `CALLVALUE` as it was in the constructor" or "`value` is always set to the `CALLVALUE` as it is during each method call":

```
constructor of C
interface constructor()

creates

address value := CALLVALUE

invariants

value == CALLVALUE
```

As currently implemented the meaning is the second meaning (the value of the env var at the time of the method invocation).

After discussing this offline for a while (as well as in [this pr](https://github.com/ethereum/act/pull/48#discussion_r497402567)), the consensus seems to be that the best approach is to seperate the `invariants` block from the `constructor` definition and to have the environment variables refer to the value of the variable during each method call.

It can however sometimes be useful to be able to refer to the constructor arguments within the `invariants` block, for example:

```
constructor of C
interface constructor(uint _totalSupply)

creates

uint totalSupply := _totalSupply

invariants

totalSupply = _totalSupply
```

It would therefore perhaps be nice to allow `invariants` blocks to refer to constructor arguments in some way. Alternatively we may with to investigate adding some kind of `pre` / `post` operators allowing us to reformulate the above `totalSupply` invariant as:

```
pre(totalSupply) == post(totalSupply)
```

No implementation files or tests are named. Start with the invariant examples and the discussion linked from PR #48; done means an agreed semantics for environment variables and constructor arguments, followed by the corresponding implementation and tests.

Written by the indexing model from the issue text.