Initial default state

Options:

1. Have a specially-named Start state. Pros: consistent naming, consistent conceptually (the contract is always in some named state). Cons: maybe this name is not actually the best name in all cases. 1.1. Require the user to define a state called Start. 1.2. The Start state is inserted by the compiler if the user does not define it.
2. Require the user to transition to a named state inside the contract constructor. Pro: flexible regarding naming, consistent conceptually (the contract is always in some named state).. Con: Extra code required.
3. Assume that the lexically first state is the start state. Pro: simple, consistent conceptually (the contract is always in some named state).. Con: depends on order of state declarations. May be unstable with refactoring.
4. Anonymous start state. Pro: simple. Con: can never be returned to.

1 seems like the best tradeoff so far. We have a rule: the Start state cannot have any fields, since otherwise we'd have to have a way of initializing them before entering the state.

contract C {
  C() {
    // Here we are already in Start state.
  }
}

The contract below shows the difficulties involved if the Start state could have fields.

contract C {
  C(int newY) {
    // Here we are already in Start state, but the state invariant has been violated.
    // We'd need to ensure that the fields got initialized in C's constructor, which is odd
    // because the fields are not lexically in scope.
  }

  state Start 
  invariant x != 0
  {
    int x;
  }
}