Grading scheme

• +1 for correct answers

• -1 for incorrect answers

Accepting the right programs

We consider the following definition of programs, as found in the lab:

Inductive Prog :=
| (* Don't modify the state. *)
  Done
| (* Add [n] to the state, then run [p]. *)
  AddThen (n : nat) (p : Prog)
| (* Multiply the state by [n], then run [p]. *)
  MulThen (n : nat) (p : Prog)
| (* Divide the state by [n], then run [p]. *)
  DivThen (n : nat) (p : Prog)
| (* Divide [n] by the state, then run [p]. *)
  VidThen (n : nat) (p : Prog)
| (* Set the state to [n], then run [p]. *)
  SetToThen (n : nat) (p : Prog).

We consider the following program validation function validate, expected to return true when the program is safe to run, i.e. when it will not incur division by zero.

Fixpoint validate' (p : Prog) (nz : bool) :=
  match p with
  | Done => true
  | AddThen 0 p => validate' p nz
  | AddThen _ p => validate' p true
  | MulThen 0 p => validate' p false
  | MulThen _ p => validate' p nz
  | DivThen 0 _ => false
  | DivThen 1 p => validate' p nz
  | DivThen _ p => validate' p false
  | VidThen _ p => nz && validate' p false
  | SetToThen 0 p => validate' p false
  | SetToThen _ p => validate' p true
  end.

Definition validate (p : Prog) : bool :=
  validate' p false.