One way of specifying the behavior of computer programs is by logical formulas that relate each program input to corresponding output. Based on this, one can then implement the specification by writing a computer program whose input/output behavior satisfies the specification. However, one would ideally like to execute the specification itself, before even writing an implementation.
In general, this is not possible. However, it becomes possible if one restricts specifications to logical formulas that have finite bounds on the size of all involved objects. Such an approach is used by the RISC Algorithm Language
The objective of this thesis topic is to write a solver that executes specifications in this language: for a given specification and given input, it computes a corresponding output. This allows a user to execute specifications in the same way as usual computer programs but, of course, with much less efficiency.