Commits

Konstantin Solomatov committed d31a218

Working through Imp.v

  • Participants
  • Parent commits b3caab4

Comments (0)

Files changed (1)

 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 *)