It looks like too big a specification, more like a wish. We could equally well write that the result must be a solution to the traveling salesman problem. A spe

It looks like too big a specification, more like a wish. We could equally well write that the result must be a solution to the traveling salesman problem. A specification can only be useful if there exist a piece of code that can take it, apply it to the algorithmic part and tell us the results. I'm thinking more along the lines of "when this field is X, that field can only be Y or Z" or "when this condition holds, these fields are not accessed". And these declarations should be a part of the main code so that it can refer to its internals.