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.
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
but never in implementations returned for code generation.
EArrayLenis 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.