ImpShort

Imp: Simple Imperative Programs

Imp Syntax

Informally, commands c are described by the following BNF grammar.
     c := skip | x := a | c ; c | if b then c else c end
         | while b do c end
As an inductive datatype in Coq:
Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

Example: Factorial

Definition fact_in_coq : com :=
  <{ Z := X;
     Y := 1;
     while Z ≠ 0 do
       Y := Y × Z;
       Z := Z - 1
     end }>.

OPTIMIZATION / REASONING DEMO

See Coq devlopment

Evaluation as a Function (Failed Attempt)

Here's an attempt at defining an evaluation function for commands, omitting the while case.
Fixpoint denote (c : com) (st : mem) : mem :=
  match c with
    | <{ skip }> ⇒
        st
    | <{ x := a }> ⇒
        (x !-> (aeval st a) ; st)
    | <{ c1 ; c2 }> ⇒
        let st' := denote c1 st in
        let st'' := denote c2 st' in
        st''
    | <{ if b then c1 else c2 end}> ⇒
        if (beval st b)
          then denote c1 st
          else denote c2 st
    | <{ while b do c end }> ⇒
        st (* bogus! *)
  end.

Relational Operational Semantics

Here is an informal definition of evaluation, presented as inference rules for readability:
   (E_Skip)  
st =[ skip ]=> st
aeval st a = n (E_Asgn)  
st =[ x := a ]=> (x !-> n ; st)
st =[ c1 ]=> st'
st' =[ c2 ]=> st'' (E_Seq)  
st =[ c1;c2 ]=> st''
beval st b = true
st =[ c1 ]=> st' (E_IfTrue)  
st =[ if b then c1 else c2 end ]=> st'
beval st b = false
st =[ c2 ]=> st' (E_IfFalse)  
st =[ if b then c1 else c2 end ]=> st'
beval st b = false (E_WhileFalse)  
st =[ while b do c end ]=> st
beval st b = true
st =[ c ]=> st'
st' =[ while b do c end ]=> st'' (E_WhileTrue)  
st =[ while b do c end ]=> st''

In Coq

Inductive ceval : com → mem → mem → Prop :=
  | E_Skip : ∀ st,
      st =[ skip ]=> st
  | E_Asgn : ∀ st a n x,
      aeval st a = n →
      st =[ x := a ]=> (x !-> n ; st)
  | E_Seq : ∀ c1 c2 st st' st'',
      st =[ c1 ]=> st' →
      st' =[ c2 ]=> st'' →
      st =[ c1 ; c2 ]=> st''
  | E_IfTrue : ∀ st st' b c1 c2,
      beval st b = true →
      st =[ c1 ]=> st' →
      st =[ if b then c1 else c2 end]=> st'
  | E_IfFalse : ∀ st st' b c1 c2,
      beval st b = false →
      st =[ c2 ]=> st' →
      st =[ if b then c1 else c2 end]=> st'
  | E_WhileFalse : ∀ b st c,
      beval st b = false →
      st =[ while b do c end ]=> st
  | E_WhileTrue : ∀ st st' st'' b c,
      beval st b = true →
      st =[ c ]=> st' →
      st' =[ while b do c end ]=> st'' →
      st =[ while b do c end ]=> st''

  where "st =[ c ]=> st'" := (ceval c st st').

Some observations

This large-step operational semantics is fine for many purposes, primary among them:
  • specifying Imp program behaviors
But there are drawbacks:
  • is partial: there is no resulting mem for a diverging program
  • isn't structural: the E_WhileTrue rule is defined in terms of itself
  • isn't executable: we can't extract this as a program (no QuickChick!)
  • is a deep embedding: no re-use of meta-level (Coq) functionality
Consequently: not very extensible, hard to re-use the metatheory.
Can we do it differently?