(* Prints out 5,4,3,2,1 *)

val P1 = 
Sequence(Assign(Var "n", IConstant 5),
	 While(Greater(Contents (Var "n"), IConstant 0),
	       Sequence(Print([Contents(Var "n")]),
 	                Assign(Var "n", Minus(Contents(Var "n"), 
					IConstant 1)))));

(* Factorial *)
val Fact =
  Sequence(Assign(Var "n", IConstant 5),
    Sequence(Assign(Var "fact", IConstant 1),
      Sequence(
	 While(Greater(Contents (Var "n"), IConstant 0),
	       Sequence(Assign(Var "fact", Times(Contents(Var "fact"),
						 Contents(Var "n"))),
 	                Assign(Var "n", Minus(Contents(Var "n"), 
					IConstant 1)))),
	 Print([Contents(Var "fact")]))));


(* to run these programs try:
    interpret P1 init_store;
    interpret Fact init_store;
*)

val p1_cxt = Cupdate(init_cxt, Var "n", aint);
val fact_cxt = Cupdate(Cupdate(init_cxt, Var "n", aint), Var "fact", aint);

(* to analyze these programs try:
    analyze(P1, p1_cxt);
    analyze(Fact, fact_cxt);
*)