Specification-only primitives

[Calvin-L]

Currently, Cozy needs to be able to generate code for every possible expression. While working on #61 it became clear that this isn't necessarily ideal; there might be a lot of benefit to having "specification-only" primitives that can appear in specifications or internal subgoals, but not in output code.

Precisely, a "specification-only" primitive may appear in

• user-written specifications
• specifications for subgoals that Cozy generates for itself
• concretization functions

but never in implementations returned for code generation.

EArrayLen is a good candidate for a specification-only primitive; it is easy to implement in Java but not in C.

This will require a nontrivial amount of work; right now Cozy is very committed to the idea that it always has a solution that it is improving. If we implement this, there will be a period where Cozy has no solution until it finds one that does not use any specification-only primitives.