# Commits

committed d31a218

Working through Imp.v

• Participants
• Parent commits b3caab4

# File Imp.v

` Qed.`
` (** [] *)`
` `
`-(** Kostik **)`
`-`
` (* ################################################### *)`
` (** ** Syntax  *)`
` `
`    your solution satisfies the test that follows. *)`
` `
` Definition pup_to_n : com := `
`-  (* FILL IN HERE *) admit.`
`+  Y ::= (ANum 0);`
`+  WHILE (BNot (BEq (AId X) (ANum 0))) DO`
`+    Y ::= (APlus (AId Y) (AId X));`
`+    X ::= (AMinus (AId X) (ANum 1))`
`+  END.`
` `
`-(* `
` Example pup_to_n_1 : `
`   test_ceval (update empty_state X 5) pup_to_n`
`   = Some (0, 15, 0).`
` Proof. reflexivity. Qed.`
`-*)`
` (** [] *)`
` `
` (** **** Exercise: 2 stars, optional (peven) *)`
`     sets [Z] to [1] otherwise.  Use [ceval_test] to test your`
`     program. *)`
` `
`-(* FILL IN HERE *)`
`+Definition is_even : com :=`
`+  Z ::= ANum 2;`
`+  WHILE BEq (AId Z) (ANum 2) DO`
`+    IFB BLe (AId X) (ANum 1)  `
`+      THEN Z ::= AId X`
`+      ELSE X ::= AMinus (AId X) (ANum 2)`
`+    FI    `
`+  END.`
`+`
`+Example is_even_239 : `
`+  test_ceval (update empty_state X 239) is_even = Some (1, 0, 1).`
`+Proof. reflexivity. Qed.`
`+`
`+Example is_even_240 : `
`+  test_ceval (update empty_state X 240) is_even = Some (0, 0, 0).`
`+Proof. reflexivity. Qed.`
`+`
` (** [] *)`
` `
`+(** Kostik **)`
`+`
` (* #################################### *)`
` (** ** Evaluation as a Relation *)`
` `