Mercurial > cpdt > repo
changeset 16:4d8ca6845e67
Source language examples
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 03 Sep 2008 15:05:21 -0400 |
parents | d8c81e19e7d3 |
children | 2c5a2a221b85 |
files | src/StackMachine.v |
diffstat | 1 files changed, 19 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/StackMachine.v Wed Sep 03 15:00:56 2008 -0400 +++ b/src/StackMachine.v Wed Sep 03 15:05:21 2008 -0400 @@ -93,6 +93,12 @@ (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *) +(** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses. *) + +Eval simpl in expDenote (Const 42). +Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)). +Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). + (** ** Target language *) @@ -145,6 +151,19 @@ end. +(** Before we set about proving that this compiler is correct, we can try a few test runs, using our sample programs from earlier. *) + +Eval simpl in compile (Const 42). +Eval simpl in compile (Binop Plus (Const 2) (Const 2)). +Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). + +(** We can also run our compiled programs and chedk that they give the right results. *) + +Eval simpl in progDenote (compile (Const 42)) nil. +Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil. +Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) nil. + + (** ** Translation correctness *) (** We are ready to prove that our compiler is implemented correctly. We can use a new vernacular command [Theorem] to start a correctness proof, in terms of the semantics we defined earlier: *)