Occam: Specification and Compiler Correctness. Part I: Simple Mathematical Interpreters