EECS 755

Software Requirements Modeling and Analysis


Array model from class

Following is the Array model of register file contents developed in class today. We will add to the model next week to capture the size of the register file.

The proofs use mostly use commands defined in class with a couple of exceptions. In some places I use trivial rather than reflexivity. trivial does a bit more work than reflexivity and can be customized. Feel free to use it in your proofs if you woule like.

I use unfold in several places where I want a function replaced by its definition. unfold f expands the definition in place. If f is defined:

Definition f(x:nat):nat := x + 1.

then unfold applied to the goal f 1 = 2 results in the goal:

1 + 1 = 2

I use unfold in a couple of places rather than simpl when simpl doesn’t work or is too involved. Note that unfold can be used on assumptions using the in syntax to specify the assumption.

Here is the [Array] module complete with proofs:

Require Import Omega.

Module Array.

  Fixpoint leb (m:nat) : nat -> bool :=
    match m with
    | O => fun _:nat => true
    | S m' =>
      fun n:nat => match n with
              | O => false
              | S n' => leb m' n'
  (** Register contents.  Either a natural number value or unknown. *)

  Inductive RC : Type :=
  | val : nat -> RC
  | unknown : RC.
  Notation "??" := unknown.

  (** Register file contents.  Function from natural to RC. *)
  Definition RFC : Type := nat -> RC.

  (** Empty register file contents *)
  Definition empty_rf:RFC := (fun n:nat => ??).

  (** [get] applies the register file function to its argument *)
  Definition get(i:nat)(f:RFC):RC := (f i).

  (** [put] uses an [if] expression to modify an existing register file *)
  Definition put(i:nat)(f:RFC)(v:RC):RFC :=
    (fun n:nat => if (beq_nat i n) then v else f n).

  (** Some tests to make sure the implementation is close to correct. *)
  Example test1: (get 3 (put 3 empty_rf (val 3))) = (val 3).
  Proof. reflexivity. Qed.

  Example test2: (get 2 (put 3 empty_rf (val 3))) = ??.
  Proof. reflexivity. Qed.

  Example test3: (get 4 (put 3 empty_rf (val 3))) = ??.
  Proof. reflexivity. Qed.

  (** Making the test slightly more abstract by checking all contents values *)
  Theorem update_position_3: forall m, (get 3 (put 3 empty_rf (val m))) = (val m).

  (** Lemma showing that [beq] is reflexive.  Will be used in a later proof *)
  Lemma beq_refl: forall i, beq_nat i i = true.
    induction i.

  (** All elements of the empty register file are unknown *)
  Theorem empty_empty: forall i , (get i empty_rf) = ??.
    intros. reflexivity.

  (** [get] applied to a [put] on the same index updates the register file
    contents.  This is correctness of the update function. *)
  Theorem update_immediate: forall v i rfc,
      (get i (put i rfc (val v))) = val v.
    unfold get.
    unfold put.
    rewrite beq_refl.

  (** [get] applied to a [put] on different indexes results in the value
    before updating.  An invariant on update. *)
  Theorem update_invariant: forall v i j rfc,
      (beq_nat j i) = false -> (get i (put j rfc (val v))) = rfc i.
    unfold get.
    unfold put.
    rewrite H.

End Array.