Enforcing that examples have outputs

[samm82]

While generating output requirements in #3259, Dr. Carette mentioned that "If you attempt to generate an output requirement with no outputs, that should be a hard error." (source) In a meeting, he also mentioned that this should be handled at a higher level than at the requirement-generation level; currently, this check is done in 15823ccc7768f998d7e54d5a9121610242b67cd5.

Alongside this, we've also been having discussion about what it means for a program to have an output, as well as the different kinds of output. In the same comment, Dr. Carette said "our concept of Output is too naïve. There are too many meanings of 'output' (ranging from the result of a function to printing on the screen). A relational specification can be refined to point to some values as being 'output'. Some theories have multiple things that can be considered 'outputs'. We should have more precise names for each of these concepts." Honestly, I'm not sure at what level this discussion should take place, but it seems related to the enforcement of programs having outputs.

The real question: assuming that each program has some sort of output (regardless of what kind of output it is), how/where should we enforce that outputs are specified for each example? Is this a valid assumption to make?

[smiths]

@samm82 my thinking is that a valid requirements document should have a requirement for some sort of output, so we could check that a valid requirements document has an output. We talked before about a project that looks for consistency/correctness checks in the requirements document. This feels like an example of that.

[JacquesCarette]

Given the current architecture assumptions we have, we're implicitly assuming there are 'outputs' of one kind or another. There are programs that don't, i.e. where no output is considered the correct behaviour. So I would not want to hard-code must have output too deeply.

Having said that, our current "language of requirements" could definitely have a consistency/correctness checker associated to it. We should run it before doing other processing on that.