(* NOTES AND IN-CLASS PRACTICE PROBLEMS FOR MIDTERM 2 *)

Require Export Smallstep(* SOL *).

(* ---------------------------------------------------------------------- *)
(* WHAT YOU SHOULD KNOW GOING INTO THE EXAM:

     - The exam is NOT cumulative -- it will focus on topics since the
       first midterm.  

     - You should understand how to formalize the operational
       semantics of a new language construct (in the style of the
       "repeat...until..." exercise)

     - You should deeply understand the Hoare rules for reasoning
       about programs and be able to construct rules for new language
       constructs (again, in the style of the "repeat...until..."
       exercise).  

     - You should be able to read and write decorated programs.

     - You should be familiar with the concept of program equivalence
       and be able to prove equivalences.

     - You should understand the concepts of the big-step (evaluation)
       and small-step (reduction) styles of operational semantics.
       You should be able to formalize a new language construct in
       either style.

     - You should be able to write proofs in the style of the
       "template for informal proofs by induction" in While.v.  If the
       midterm asks for any informal proofs, your answers will be
       expected to follow this format PRECISELY.

     - You should understand the rest of this file. :-)

LATE ADDITIONS:

     - You should understand and be able to calculate weakest preconditions. 

     - You should understand all the major properties of the big-step
       and small-step relations we've looked at, and be able to prove
       them (determinacy, progress, etc.)

*)

(* ---------------------------------------------------------------------- *)
(* Small-step presentation of IMP *)

Inductive astep : state -> aexp -> aexp -> Prop :=
  | ASId : forall st i, 
    astep st (AId i) (ANum (st i))
  | ASPlus : forall st n1 n2,
    astep st ((ANum n1) +++ (ANum n2)) (ANum (plus n1 n2))
  | ASPlus1 : forall st a1 a1' a2,
    astep st a1 a1' ->
    astep st (a1 +++ a2) (a1' +++ a2)
  | ASPlus2 : forall st n1 a2 a2',
    astep st a2 a2' ->
    astep st ((ANum n1) +++ a2) ((ANum n1) +++ a2')
  | ASMinus : forall st n1 n2,
    astep st ((ANum n1) --- (ANum n2)) (ANum (minus n1 n2))
  | ASMinus1 : forall st a1 a1' a2,
    astep st a1 a1' ->
    astep st (a1 --- a2) (a1' --- a2)
  | ASMinus2 : forall st n1 a2 a2',
    astep st a2 a2' ->
    astep st ((ANum n1) --- a2) ((ANum n1) --- a2')
  | ASMult : forall st n1 n2,
    astep st ((ANum n1) *** (ANum n2)) (ANum (mult n1 n2))
  | ASMult1 : forall st a1 a1' a2,
    astep st a1 a1' ->
    astep st (a1 *** a2) (a1' *** a2)
  | ASMult2 : forall st n1 a2 a2',
    astep st a2 a2' ->
    astep st ((ANum n1) *** a2) ((ANum n1) *** a2').

Inductive bstep : state -> bexp -> bexp -> Prop :=
  | BSEq : forall st n1 n2,
    bstep st (ANum n1 === ANum n2) 
             (if (beq_nat n1 n2) then BTrue else BFalse)
  | BSEq1 : forall st a1 a1' a2,
    astep st a1 a1' ->
    bstep st (a1 === a2) (a1' === a2)
  | BSEq2 : forall st n1 a2 a2',
    astep st a2 a2' ->
    bstep st (ANum n1 === a2) (ANum n1 === a2')
  | BSLtEq : forall st n1 n2,
    bstep st (ANum n1 <<= ANum n2) 
             (if (ble_nat n1 n2) then BTrue else BFalse)
  | BSLtEq1 : forall st a1 a1' a2,
    astep st a1 a1' ->
    bstep st (a1 <<= a2) (a1' <<= a2)
  | BSLtEq2 : forall st n1 a2 a2',
    astep st a2 a2' ->
    bstep st (ANum n1 <<= a2) (ANum n1 <<= a2')
  | BSNotTrue : forall st,
    bstep st (BNot BTrue) BFalse
  | BSNotFalse : forall st,
    bstep st (BNot BFalse) BTrue
  | BSNotStep : forall st b1 b1',
    bstep st b1 b1' ->
    bstep st (BNot b1) (BNot b1')
  | BSAndTrueTrue : forall st,
    bstep st (BAnd BTrue BTrue) BTrue
  | BSAndTrueFalse : forall st,
    bstep st (BAnd BTrue BFalse) BFalse
  | BSAndFalse : forall st b2,
    bstep st (BAnd BFalse b2) BFalse
  | BSAndTrueStep : forall st b2 b2',
    bstep st b2 b2' ->
    bstep st (BAnd BTrue b2) (BAnd BTrue b2')
  | BSAndStep : forall st b1 b1' b2,
    bstep st b1 b1' ->
    bstep st (BAnd b1 b2) (BAnd b1' b2)
  | BSOrFalseFalse : forall st,
    bstep st (BOr BFalse BFalse) BFalse
  | BSOrFalseTrue : forall st,
    bstep st (BOr BFalse BTrue) BTrue
  | BSOrTrue : forall st b2,
    bstep st (BOr BTrue b2) BTrue
  | BSOrFalseStep : forall st b2 b2',
    bstep st b2 b2' ->
    bstep st (BOr BFalse b2) (BOr BFalse b2')
  | BSOrStep : forall st b1 b1' b2,
    bstep st b1 b1' ->
    bstep st (BOr b1 b2) (BOr b1' b2).

Inductive cstep : state -> com -> com -> state -> Prop :=
  | CSAssStep : forall st i a a',
    astep st a a' ->
    cstep st (CAss i a) (CAss i a') st
  | CSAss : forall st i n, 
    cstep st (CAss i (ANum n)) CSkip (override st i n)
  | CSSeqStep : forall st c1 c1' st' c2,
    cstep st c1 c1' st' ->
    cstep st (CSeq c1 c2) (CSeq c1' c2) st'
  | CSSeqFinish : forall st c2,
    cstep st (CSeq CSkip c2) c2 st
  | CSIfTrue : forall st c1 c2,
    cstep st (CIf BTrue c1 c2) c1 st
  | CSIfFalse : forall st c1 c2,
    cstep st (CIf BFalse c1 c2) c2 st
  | CSIfStep : forall st b b' c1 c2,
    bstep st b b' ->
    cstep st (CIf b c1 c2) (CIf b' c1 c2) st
  | CSWhile : forall st b c1,
    cstep st (CWhile b c1) (CIf b (CSeq c1 (CWhile b c1)) CSkip) st.

(* ---------------------------------------------------------------------- *)
(* SOME MORE HOARE-LOGIC PROOFS TO WORK TOGETHER *)

(*
RECALL: The GREATEST COMMON DIVISOR of two numbers x and y, written
gcd(x,y), is the largest number that evenly divides both x and y.

SOME USEFUL FACTS:

  If y1>y2 then gcd(y1,y2)=gcd(y1-y2,y2)
  If y2>y1 then gcd(y1,y2)=gcd(y1,y2-y1)
  If y1=y2 then gcd(y1,y2)=y1=y2

EUCLID'S ALGORITHM FOR CALCULATING GCDs:

  X ::= x;
  Y ::= y;
  while BNot (!X===!Y) do (
    (testif !Y <<= !X 
      then 
         X ::= !X --- !Y 
      else 
         Y ::= !Y --- !X
    )
  )

SPECIFICATION:

                          { True }
  X ::= x;
  Y ::= y;
  while BNot (!X===!Y) do (
    (testif !Y <<= !X 
      then 
         X ::= !X --- !Y 
      else 
         Y ::= !Y --- !X
    )
  )
                          { X = gcd(x,y) }


DECORATED PROGRAM:

                          { True } =>
                          { gcd(x,y)=gcd(x,y) }
X ::= x;
                          { gcd(x,y)=gcd(X,y) }
Y ::= y;
                          { gcd(x,y)=gcd(X,Y) }
while BNot (!X===!Y) do (
                          { gcd(x,y)=gcd(X,Y) /\ X<>Y }
  (testif !Y <<= !X 
    then 
                          { gcd(x,y)=gcd(X,Y) /\ X<>Y /\ Y<=X } =>
                          { gcd(x,y)=gcd(X,Y) /\ Y<X } =>
                          { gcd(x,y)=gcd(X-Y,Y)
       X ::= !X --- !Y 
                          { gcd(x,y)=gcd(X,Y) }
    else 
                          { gcd(x,y)=gcd(X,Y) /\ X<>Y /\ ~(Y<=X) } =>
                          { gcd(x,y)=gcd(X,Y) /\ X<Y } =>
                          { gcd(x,y)=gcd(X,Y-X)
       Y ::= !Y --- !X
                          { gcd(x,y)=gcd(X,Y) }
  )
                          { gcd(x,y)=gcd(X,Y) }
)
                          { gcd(x,y)=gcd(X,Y) /\ ~(X<>Y) } =>
                          { gcd(x,y)=gcd(X,Y) /\ X=Y } =>
                          { gcd(x,y)=gcd(X,X) } =>
                          { X = gcd(x,y) }
*)

(* ---------------------------------------------- *)
(* Absurdly slow multiplication *)

(*

PROGRAM AND SPEC:

                            { X = x } =>
Z ::= A0;
while BNot (!X===A0) do (
  W ::= ANum y;
  while BNot (!W===A0) do (
    Z ::= !Z +++ A1;
    W ::= !W --- A1
  );
  X ::= !X --- A1
)
                            { Z = x * y }


DECORATED PROGRAM:

                      { X = x } =>
                      { 0 = (x-X) * y /\ X<=x } 
Z ::= A0;
                      { Z = (x-X) * y /\ X<=x } 
while BNot (!X===A0) 
do (
                      { Z = (x-X) * y /\ X<=x /\ X<>0 } =>
                      { Z = (x-X) * y + (y-y) /\ X<=x /\ X<>0 } 
  W ::= ANum y;
                      { Z = (x-X) * y + (y-W) /\ X<=x /\ W<=y /\ X <> 0} 
  while BNot (!W===A0)
  do (
                      { Z = (x-X) * y + (y-W) /\ X<=x /\ X <> 0 
                                            /\ W<=y /\ W<>0 } =>
                      { Z + 1 = (x-X) * y + (y-W) + 1 
                                            /\ X<=x /\ X <> 0 
                                            /\ W-1<=y /\ W<>0 } =>
                      { Z + 1 = (x-X) * y + (y-(W-1)) \
                                            /\ X<=x /\ X <> 0 /\ W-1<=y }
    Z ::= !Z +++ A1;
                      { Z = (x-X) * y + (y-(W-1)) /\ X<=x /\ X <> 0 /\ W-1<=y }
    W ::= !W --- A1
                      { Z = (x-X) * y + (y-W) /\ X<=x /\ X <> 0 /\ W<=y }
  );
                      { Z = (x-X) * y + (y-W) /\ X<=x /\ X <> 0 /\ W<=y /\ ~(W<>0) } => 
                      { Z = (x-X) * y + y /\ X<=x /\ X <> 0 } =>  
                      { Z = ((x-X)+1) * y /\ X<=x /\ X <> 0 } =>  
                      { Z = (x-(X-1)) * y /\ X<=x }
  X ::= !X --- A1
                      { Z = (x-X) * y /\ X<=x }
)
                      { Z = (x-X) * y /\ X<=x /\ ~(X<>0) } =>
                      { Z = (x-X) * y /\ X=0 } =>
                      { Z = x * y }
*)