Grading scheme

• +1 for correct answers

• -0.5 for incorrect answers

Tribools

Consider the following definitions:

Inductive tribool := yes | no | maybe.

Definition And (x y: tribool) : tribool :=
  match x, y with
  | yes, yes | yes, maybe | maybe, yes => yes
  | maybe, maybe => maybe
  | _, _ => no
  end.

Definition Or (x y : tribool) : tribool :=
  match x, y with
  | yes,   _ | _, yes   => yes
  | maybe, _ | _, maybe => maybe
  | _, _ => no
  end.

Definition Neg (x: tribool): tribool :=
  match x with
  | yes => no
  | maybe => maybe
  | no => yes
  end.

Which of the following properties are true?

Soundness and completeness

Consider the following definitions:

Definition IfSafeThenValid :=
  forall p, safe p -> validate p = true.

Definition IfValidThenSafe :=
  forall p, validate p = true -> safe p.

Rejecting the right programs

We wish to extend our simple language with an additional constructor for subtraction, SubThen. SubThen n p subtracts n from the state then runs p. The semantics of each construct is described in comments:

Inductive Prog :=
| (* Don't modify the state. *)
  Done
| (* Add [n] to the state, then run [p]. *)
  AddThen (n : nat) (p : Prog)
| (* Subtract [n] from the state, then run [p]. *)
  SubThen (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).

Note that subtraction saturates at 0, i.e. if n < m, then n - m = 0.

We consider the following program-validation function validate, intended to reject (return false for) every unsafe program. In other words, if validate accepts (returns true for) p, then p should be be safe to run with any input (i.e. it will never trigger a 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
  | SubThen _ p   => validate' p nz
  | 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.