Library ProgramAssertions

Instructions and structures representing programs.

@author Patryk Czarnik

Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Program.
Require Import RuntimeStructures.
Require Import Sem_Frame.
Require Import Relations.

Program assertions

Module Type PROGRAM_ASSERTIONS.

Included modules

  Declare Module M_Sem_Frame : SEM_FRAME.

  Import M_Sem_Frame.
  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_Program.
  Import M_RuntimeStructures.

  Open Local Scope type_scope.

Frame-level assertions

An assertion is a property of a state, here a frame.

Definition TCodeAssertion := TFrame → Prop.

A set of annotations assigned to instructions (or rather "places") within a method body.

Parameter TCodeAssertions: Type.

Returns assertion assigned to a given position in method body, if any.

Parameter getCodeAssertion: TCodeAssertions → TPC → option TCodeAssertion.

Returns assertion from a given position enriched with a statement that the given position is the current point of execution.

  Definition getPositionedAssertion (asserts: TCodeAssertions) (pc: TPC) : TCodeAssertion :=
    fun frame ⇒
    match getCodeAssertion asserts pc with
    | None ⇒ False
    | Some assert ⇒ frameGetPC frame = pc ∧ (assert frame )
    end.

A method body is "described" if assertions are specified for (positions of) all instructions.

  Definition codeDescribed (code: TCode) (asserts: TCodeAssertions) :=
    ∀ pc,
      (∃ instr, getInstruction code pc = Some instr )
        ↔
      (∃ assert, getCodeAssertion asserts pc = Some assert ).

Helper lemma about getPositionedAssertion.

  Lemma positionedAssertionPc: ∀ asserts pc frame,
    getPositionedAssertion asserts pc frame →
    frameGetPC frame = pc.
  Proof.
    intros.
    unfold getPositionedAssertion in H.
    destruct (getCodeAssertion asserts pc); tauto.
  Qed.

A given state (at frame level) is described by (at least) one of assertions.

  Definition frameDescribed (asserts: TCodeAssertions) (frame: TFrame) :=
    ∃ pc,
    getPositionedAssertion asserts pc frame.

A given state (at frame level) is described by the assertion corresponding to the position pointed by the state.

Definition frameDescribed2 (asserts: TCodeAssertions) (frame: TFrame) :=
getPositionedAssertion asserts (frameGetPC frame) frame.

The two formulations of "being described" are equivalent.

  Lemma frameDescribed_equiv: ∀ asserts frame,
    frameDescribed asserts frame ↔ frameDescribed2 asserts frame.
  Proof.
    unfold frameDescribed, frameDescribed2.
    intros.
    split.
    intros.
    destruct H as [pc H].
    replace pc with (frameGetPC frame) in ×.
    assumption.
    eapply positionedAssertionPc.
    eassumption.

    intros.
    ∃ (frameGetPC frame).
    assumption.
  Qed.

Logic to prove partial correctness

A property expressing that a given set of assertions is sound wrt a given method body:

Any step from any described state yields to a state which is also described.

  Definition singleTransitions (code: TCode) (asserts: TCodeAssertions) :=
    ∀ frame1 frame2,
      frameDescribed asserts frame1 →
      stepFrame code frame1 frame2 →
      frameDescribed asserts frame2.

If a method is properly specified (in the sense of singleTransitions, than any reachable state is "proper" (described by an appropriate assertion).

  Theorem multiTransitions: ∀ code asserts frame1 frame2,
    singleTransitions code asserts →
    frameDescribed asserts frame1 →
    stepsFrame code frame1 frame2 →
    frameDescribed asserts frame2.
  Proof.
    intros code asserts frame1 frame2 HSingleTrans HFrame1 HSteps.
    apply clos_rt_rtn1 in HSteps.
    induction HSteps.
    apply HFrame1.

    eapply HSingleTrans.
    apply IHHSteps.
    apply H.
  Qed.
End PROGRAM_ASSERTIONS.

Creating programs with assertions

Module of this type enables creating assertion sets from lists.

Module Type PROGRAM_ASSERTIONS_W_CONSTRUCTORS.
  Include PROGRAM_ASSERTIONS.
  Require Import List.
  Import M_Sem_Frame.
  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_Program.
  Import M_RuntimeStructures.

  Open Local Scope type_scope.

Creates a code block annotation containing the given assertions in the given order.

Parameter assertionsFromList: list TCodeAssertion → TCodeAssertions.

PC relates directly to the position of assertion on the list.

  Axiom PgetInstructionIffNth: ∀ li pc,
    getCodeAssertion (assertionsFromList li) pc =
    nth_error li (pcToPosition pc).

  Lemma frameDescribed_inRange: ∀ li frame,
    frameDescribed (assertionsFromList li) frame →
    pcToPosition (frameGetPC frame) < length li.
  Proof.
    unfold frameDescribed.
    unfold getPositionedAssertion.
    intros.
    destruct H as [pc H].
    rewrite PgetInstructionIffNth in H.
    case_eq (nth_error li (pcToPosition pc)).
    intros a Heq.
    rewrite Heq in H.
    eapply Pnth_error_length.
    rewrite (proj1 H).
    eassumption.
    intros Heq.
    rewrite Heq in H.
    contradiction.
  Qed.
End PROGRAM_ASSERTIONS_W_CONSTRUCTORS.