PVS‎ > ‎examples‎ > ‎


This example was originally implemented at LaBRI, in year 2000, and used as a Coq and PVS Master student project, see LaBRI 3 May 2000 note.

Correctness of a simple compiler of algebraic expressions

This is a pedagogical example illustrating proof techniques for functional programming, and the newly available PVS ground evaluator (that came out with PVS 2.4). The compiler is a function that translates expressions such as
plus(v(10), mult(v(17), v(10)))
into machine code such as
(: load(r(0), l(10)),
   load(r(1), l(17)),
   load(r(2), l(10)),
   mult(r(1), r(2)),
   add(r(0), r(1))   :)    .
The compiler is constructive so that PVS ground evaluator can actually be used to generate the above machine code from the form:
compile(plus(v(10), mult(v(17), v(10))))    .
The compiler is proved correct, meaning that evaluating the source expression or the object code in equivalent environments will always produce the same value (in register r(0) for the object code). More precisely:

compiler_correctness: THEOREM
      (FORALL (me: machine.environment, ee: expressions.environment,
               e: expression):
         equivalent?(me, ee)
         eval(compile(e))(me)(r(0)) = eval(e)(ee)) ;


The compiler has been adapted to PVS 2.4, then to PVS 5.0: