Over the past two weeks, we've begun applying the mathematical tools developed in the first part of the course to studying the theory of a small programming language. (This language is often called Imp, since it is a language of pure imperative programs.)

• We defined a type of abstract syntax trees for Imp, together with an evaluation relation (a partial function on states) that specifies the operational semantics of programs.
  
  If the course had ended at this point, we would still have gotten to something extremely useful: a set of tools for defining and discussing programming languages and language features that are mathematically precise, easy to work with, and very flexible.
  
  The language we defined, though small, captures some of the key features of full-blown languages like C, C++, and Java, including the fundamental notion of mutable state and some common control structures.
  
  
• We proved a number of metatheoretic properties ("meta" in the sense that they are properties of the language as a whole, rather than properties of particular programs in the language), including:
  
  
  • determinacy of evaluation
    
    
  • equivalence of some different ways of writing down the definition
    
    
  • guaranteed termination of certain classes of programs
    
    
  • correctness (in the sense of preserving behavioral equivalence) of a number of useful program transformations
    
    
  All of these properties -- especially the behavioral equivalences -- are things that language designers, compiler writers, and users really care about knowing. Indeed, many of them are so fundamental to our understanding of the programming languages we deal with that we may not consciously recognize them as "theorems." But, as the discussion of subst_equiv_property showed, properties that seem intuitively obvious can sometimes be quite subtle or, in some cases, actually even wrong!
  
  We'll return to this theme later in the course when we discuss types and type soundness.
  
  
• We saw a couple of examples of program verification -- using the precise definition of Imp to prove formally that certain particular programs (factorial and slow subtraction) satisfied particular specifications of their behavior.

This week, we're going to take this idea further. We'll develop a reasoning system called Floyd-Hoare Logic (often shortened to just Hoare Logic), in which each of the syntactic constructs of Imp is equipped with a single, generic "proof rule" that can be used to reason about programs involving this construct.

Hoare Logic has a long history, dating back to the 1960s, and it has been the subject of intensive research right up to the present day. It lies at the core of a huge variety of tools that are now being used to specify and verify real software systems.

Assertions

If we're going to talk about specifications of programs, the first thing we'll want is a way of making assertions about properties that hold at particular points in time -- i.e., properties that may or may not be true of a given state.

Exercise: 1 star (assertions)

Paraphrase the following assertions in English.

      fun st => st X = 3
      fun st => st X = x
      fun st => st X <= st Y
      fun st => st X = 3 \/ st X <= st Y
      fun st => (mult (st Z) (st Z)) <= x
                 /\ ~ ((mult (S (st Z)) (S (st Z))) <= x)
      fun st => True
      fun st => False

(Remember that one-star exercises do not need to be handed in.)

☐

This way of writing assertions is correct -- it precisely captures what we mean, and it is exactly what we will use in Coq proofs -- but it is not very nice to look at: every single assertion that we ever write is going to begin with fun st => , and everyplace we refer to a variable in the current state it is written st X.

Moreover, this is the *only* way we use states and the only way we refer to the values of variables in the current state. (We never need to talk about two states at the same time, etc.) So when we are writing down assertions in informal contexts, we can make some simplifications: drop the initial fun st => and write just X instead of st X. For example, instead of

      fun st => (mult (st Z) (st Z)) <= x
                 /\ ~ ((mult (S (st Z)) (S (st Z))) <= x)

we'll write just

      (mult Z Z) <= x /\ ~ ((mult (S Z) (S Z)) <= x).

Hoare triples

Next, we need a way of specifying -- making a general claim about -- the behavior of a command. Since we've defined assertions as a way of making general claims about the properties of states, and since the behavior of a command is to transform one state to another, a general claim about a command takes the following form:

• "If c is started in a state satisfying assertion P, then when (and if) c terminates, the final state is guaranteed to satisfy the assertion Q."

Such a claim is called a Hoare Triple. The property P is called a precondition, and Q is a postcondition.

Since we'll be working a lot with Hoare triples, it's useful to have a compact notation:

       {{ P }} c {{ Q }}.

(Traditionally, Hoare triples are written {P} c {Q}, but single braces are already used in Coq.)

Exercise: 1 star (triples)

Paraphrase the following Hoare triples in English. (Note that we're using the informal convention for writing down assertions.)

      {{True}} c {{X = 5}}

      {{X = x}} c {{X = plus x 5)}}

      {{X <= Y}} c {{Y <= X}}

      {{True}} c {{False}}

      {{X = x}}
      c
      {{Y = real_fact x}}.

      {{True}}
      c
      {{(mult Z Z) <= x /\ ~ ((mult (S Z) (S Z)) <= x)}}

☐

Exercise: 1 star (valid_triples)

Which of the following Hoare triples are valid (i.e., the claimed relation between P, c, and Q is true)?

      {{True}} X ::= A5 {{X = 5}}

      {{X = 2}} X ::= !X +++ 1 {{X = 3}}

      {{True}} X ::= A5; Y ::= A0 {{X = 5}}

      {{X = 2 /\ X = 3}} X ::= A5 {{X = 0}}

      {{True}} SKIP {{False}}

      {{False}} SKIP {{True}}

      {{True}} WHILE BTrue DO SKIP LOOP {{False}}

      {{X = 0}} WHILE !X === A0 DO X ::= !X +++ 1 LOOP {{X = 1}}

      {{X = 1}}
      WHILE BNot (!X === A0) DO X ::= !X +++ 1 LOOP
      {{X = 100}}

☐

To get us warmed up, here are two simple lemmas about Hoare triples

Weakest preconditions

Some Hoare triples are more interesting than others. For example,

      {{ False }} X ::= !Y + A1 {{ X <= 5 }}

is perfectly valid, but it tells us nothing useful -- in particular, it doesn't tell us how we can use the command X ::= !Y + A1 to achieve the postcondition X <= 5.

By contrast,

      {{ Y <= 4 /\ Z = 0 }} X ::= !Y + A1 {{ X <= 5 }}

is useful: it tells us that, if we can somehow create a situation in which we know that Y <= 4 /\ Z = 0, then running this command will produce a state satisfying this postcondition. However, this triple is still not as useful as it could be, because the Z = 0 clause in the precondition actually has nothing to do with the postcondition X <= 5. The *most* useful triple (with the same command and postcondition) is this one:

      {{ Y <= 4 }} X ::= !Y + A1 {{ X <= 5 }}

We say that Y <= 4 is the weakest precondition of the command X ::= !Y + A1 for the postcondition X <= 5.

In general, we say that "P is the weakest precondition of c for Q" if

• {{P}} c {{Q}}, and
  
  
• if P' is an assertion such that {{P'}} c {{Q}}, then, for all states st, P' st implies P st.

That is, P suffices to guarantee that Q holds after c, and P is the weakest (easiest to satisfy) assertion that guarantees Q after c.

Exercise: 1 star (wp)

What are the weakest preconditions of the following commands for the following postconditions?

     {{ ? }} SKIP {{ X = 5 }}

     {{ ? }} X ::= !Y +++ !Z {{ X = 5 }}

     {{ ? }} X ::= !Y {{ X = Y }}

     {{ ? }}
       IFB !X === A0
       THEN Y ::= !Z +++ A1
       ELSE Y ::= !W +++ A2
     {{ Y = 5 }}

     {{ ? }}
       X ::= 5
     {{ X = 0 }}

     {{ ? }}
       WHILE BTrue DO X LOOP ::= 0
     {{ X = 0 }}

☐

Proof rule for assignment

The rule for reasoning about assignment is the most basic of the Hoare rules... and probably the trickiest! Here's how it works.

Consider this (valid) Hoare triple:

       {{ Y = 1 }} X ::= !Y {{ X = 1 }}

In English: if we start out in a state where the value of Y is 1 and we assign !Y to X, then we'll finish in a state where X is 1. That is, the property of being equal to 1 gets transferred from Y to X.

Similarly, in

       {{ Y + Z = 1 }} X ::= !Y +++ !Z {{ X = 1 }}

the same property (being equal to one) gets transferred to X from the expression !Y +++ !Z on the right-hand side of the assignment.

More generally, if a is *any* arithmetic expression, then

       {{ a = 1 }} X ::= a {{ X = 1 }}

is a valid Hoare triple.

Even more generally, if P is *any* property of numbers and a is any arithmetic expression, then

       {{ P(a) }} X ::= a {{ P(X) }}

is a valid Hoare triple.

Rephrasing this a bit leads us to the general Hoare rule for assignment:

      {{ P where a is substituted for X }} X ::= a {{ P }}

This rule looks backwards to everyone at first -- what it's saying is that, if P holds in an environment where X is replaced by the value of a, then P still holds after executing X ::= a.

For example, these are valid applications of the assignment rule:

      {{ X + 1 <= 5 }} X ::= !X +++ A1 {{ X <= 5 }}

      {{ 3 = 3 }} X ::= A3 {{ X = 3 }}

      {{ 0 <= 3 /\ 3 <= 5 }} X ::= A3 {{ 0 <= X /\ X <= 5 }}

We could try to formalize the assignment rule directly in Coq by treating P as a family of assertions indexed by arithmetic expressions -- something like this:

      Theorem hoare_asgn_firsttry :
        forall (P : aexp -> Assertion) V a,
        {{fun st => P a st}} (V ::= a) {{fun st => P (AId V) st}}.

But this formulation is not very nice, for two reasons. First, it is not clear how we'd prove it is valid (we'd need to somehow reason about all possible propositions). And second, even if we could prove it, it would be awkward to use.

A much smoother way of formalizing the rule arises from the following obervation:

• For all states st, "P where a is substituted for X" holds in the state st if and only if P holds in the state override st V (aeval st a).

That is, asserting that a substituted variant of P holds in some state is the same as asserting that P itself holds in a substituted variant of the state.

Substitution:

The proof rule for assignment:

Here's a first formal proof using this rule:

Unfortunately, the hoare_asgn rule doesn't literally apply to the initial goal: it only works with triples whose precondition has precisely the form assn_sub P V a for some P, V, and a. So we start with asserting a little lemma to get the goal into this form.

Doing this kind of fiddling with the goal state every time we want to use hoare_asgn would gets tiresome pretty quickly. Fortunately, there are easier alternatives. One simple one is to state a slightly more general theorem that introduces an explicit equality hypothesis:

With this version of hoare_asgn, we can do the proof much more smoothly.

Exercise: 2 stars (hoare_asgn_examples)

Translate these informal Hoare triples:

       {{ X + 1 <= 5 }} X ::= !X +++ A1 {{ X <= 5 }}

       {{ 0 <= 3 /\ 3 <= 5 }} X ::= A3 {{ 0 <= X /\ X <= 5 }}

into formal statements and use hoare_asgn_eq to prove them.

☐

Exercise: 3 stars (hoarestate2)

If the assignment rule still seems "backward", it may help to think a little about alternative "forward" rules. Here is a seemingly natural one:

      {{ True }} X ::= a {{ X = a }}

Explain what is wrong with this rule.

(* FILL IN HERE *)

☐

Rules of consequence

The above discussion about the awkwardness of applying the assignment rule illustrates a more general point: sometimes the preconditions and postconditions we get from the Hoare rules won't quite be the ones we want -- they may (as in the above example) be logically equivalent but have a different syntactic form that fails to unify with the goal we are trying to prove, or they actually may be logically weaker or stronger than the goal.

For instance, while

      {{3 = 3}} (X ::= A3) {{X = 3}},

is a valid Hoare triple, what we probably have in mind when we think about the effect of this assignment is something more like this:

      {{True}} (X ::= A3) {{X = 3}}.

This triple is also valid, but we can't derive it from hoare_asgn (or hoare_asgn_eq) because True and 3 = 3 are not equal, even after simplification.

In general, if we can derive {{P}} c {{Q}}, it is valid to change P to P' as long as P' is still enough to show P, and change Q to Q' as long as Q is enough to show Q'.

This observation is captured by the following Rule of Consequence.

                {{P'}} c {{Q'}}
         P implies P' (in every state)
         Q' implies Q (in every state)
         -----------------------------
                {{P}} c {{Q}}

For convenience, here are two more consequence rules -- one for situations where we want to just strengthen the precondition, and one for when we want to just loosen the postcondition.

                {{P'}} c {{Q}}
         P implies P' (in every state)
         -----------------------------
                {{P}} c {{Q}}

                {{P}} c {{Q'}}
         Q' implies Q (in every state)
         -----------------------------
                {{P}} c {{Q}}

For example, we might use (the "_pre" version of) the consequence rule like this:

                {{ True }} =>
                {{ 1 = 1 }}
    X ::= A1
                {{ X = 1 }}

Or, formally...

The eapply tactic

This is a good moment to introduce another convenient feature of Coq. Having to write P' explicitly in the example above is a bit annoying because the very next thing we are going to do -- applying the hoare_asgn rule -- is going to determine exactly what it should be. We can use eapply instead of apply to tell Coq, essentially, "The missing part is going to be filled in later."

In general, eapply H tactic works just like apply H except that, instead of failing if unifying the goal with the conclusion of H does not determine how to instantiate all of the variables appearing in the premises of H, eapply H will replace these variables with existential variables (written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof.

There is also an eassumption tactic that works similarly.

Informally:

                   {{ True }} =>
                   {{ a = a }}
    X ::= a
                   {{ X = a }}

Proof rule for SKIP

Now we come to some easier rules...

Since SKIP doesn't change the state, it preserves any property P:

      {{ P }} SKIP {{ P }}

Proof rule for ;

More interestingly, if the command c1 takes any state where P holds to a state where Q holds, and if c2 takes any state where Q holds to one where R holds, then doing c1 followed by c2 will take any state where P holds to one where R holds:

        {{ P }} c1 {{ Q }}
        {{ Q }} c2 {{ R }}
       ---------------------
       {{ P }} c1;c2 {{ R }}

Note that, in the formal rule hoare_seq, the premises are given in "backwards" order (c2 before c1). This matches the natural flow of information in many of the situations where we'll use the rule.

Informally, a nice way of recording a proof using this rule is as a "decorated program" where the intermediate assertion Q is written between c1 and c2:

                   {{ a = n }}
    X ::= a;
                   {{ X = n }} <---- Q
    SKIP
                   {{ X = n }}

Exercise: 2 stars (hoare_asgn_example4)

Translate this decorated program into a formal proof:

                   {{ True }} =>
                   {{ 1 = 1 }}
    X ::= A1;
                   {{ X = 1 }} =>
                   {{ X = 1 /\ 2 = 2 }}
    Y ::= A2
                   {{ X = 1 /\ Y = 2 }}

☐

Exercise: 3 stars, optional (swap_exercise)

Write an IMP program c that swaps the values of X and Y and show (in Coq) that it satisfies the following specification:

      {{X <= Y}} c {{Y <= X}}

☐

Exercise: 3 stars, optional (hoarestate1)

Explain why the following proposition can't be proven:

      forall (a : aexp) (n : nat),
         {{fun st => aeval st a = n}} (X ::= A3; Y ::= a)
         {{fun st => st Y = n}}.

☐

Proof rule for conditionals

What sort of rule do we want for reasoning about conditional commands? Certainly, if the same assertion Q holds after executing either branch, then it holds after the whole conditional. So we might be tempted to write:

              {{P}} c1 {{Q}}
              {{P}} c2 {{Q}}
      --------------------------------
      {{P}} IFB b THEN c1 ELSE c2 {{Q}}

However, this is rather weak. For example, using this rule, we cannot show that:

                             {{True}}
     IFB !X === A0
     THEN Y ::= A2
     ELSE Y ::= !X +++ 1
                             {{ X <= Y }}

since the rule tells us nothing about the state in which the assignments take place in the then- and else- branches.

But, actually, we can say something more precise. In the "then" branch, we know that the boolean expression b evaluates to true, and in the "else" branch, we know it evaluates to false. Making this information available in the premises of the lemma gives us more information to work with when reasoning about the behavior of c1 and c2 (i.e., the reasons why they establish the postcondtion Q).

           {{P /\ b}} c1 {{Q}}
           {{P /\ ~b}} c2 {{Q}}
      --------------------------------
      {{P}} IFB b THEN c1 ELSE c2 {{Q}}

To interpret this rule formally, we need to do a little work.

Strictly speaking, what we've written -- P /\ b -- is the conjunction of an assertion and a boolean expression, which doesn't typecheck. To fix this, we need a way of formally "lifting" any bexp b to an assertion. We'll write bassn b for the assertion "b evaluates to true in (a given state)."

A couple of facts about bassn will be useful in proving the validity of the proof rule for conditionals.

Now we can formalize the Hoare proof rule for conditionals (and prove it correct).

Proof rule for loops

Finally, we need a rule for reasoning about while loops.

Suppose we have a loop

      WHILE b DO c LOOP

and we want to find a pre-condition P and a post-condition Q such that

      {{P}} WHILE b DO c LOOP {{Q}}

is a valid triple.

First of all, let's think about the case where b is false at the beginning, so that the loop body never executes at all. In this case, the loop behaves like SKIP, so we might be tempted to write

      {{P}} WHILE b DO c LOOP {{P}}.

But, as we remarked above for the conditional, we know a little more at the end -- not just P, but also the fact that b is false in the current state. So we can enrich the postcondition a little:

      {{P}} WHILE b DO c LOOP {{P /\ ~b}}

What about the case where the loop body DOES get executed? In order to ensure that P holds when the loop finally exits, we certainly need to make sure that the command c guarantees that P holds whenever c is finished. Moreover, since P holds at the beginning of the first execution of c, and since each execution of c re-establishes P when it finishes, we can always assume that P holds at the beginning of c. This leads us to the following rule:

                   {{P}} c {{P}}
        -----------------------------------
        {{P}} WHILE b DO c LOOP {{P /\ ~b}}

This is almost the rule we want, but again it can be improved a little: at the beginning of the loop body, we know not only that P holds, but also that the guard b is true in the current state. This gives us a little more information to use in reasoning about c. Here is the final version of the rule:

               {{P /\ b}} c {{P}}
        -----------------------------------
        {{P}} WHILE b DO c LOOP {{P /\ ~b}}

The proposition P is called an invariant.

Formalizing the rule in Coq...

Decorated programs

There are only a few places where we actually need to think when performing a correctness proof in Hoare Logic. (In fact, the last two are the only places where real creativity is required.)

• the intermediate assertion for a sequential composition c1;c2
  
  
• the "inner" assertions P' and Q' in the consequence rules
  
  
• the invariant of a while loop
  
  
• the outermost pre- and post-conditions

We can completely remove the need for thinking by decorating programs with appropriate assertions in these situations (as we've already in several places above). Such a decorated program carries with it an (informal) proof of its own correctness.

Concretely, a decorated program has one of the following forms:

• null program
  
                           {{ P }}
            SKIP
                           {{ P }}
  
  
• sequential composition:
  
                           {{ P }}
            c1;
                           {{ Q }}
            c2
                           {{ R }}
  
  (where c1 and c2 are decorated programs)
  
  
• assignment:
  
                           {{ P where a is substituted for V }}
            V ::= a
                           {{ P }}
  
  
• conditional:
  
                           {{ P }}
            IFB b THEN
                           {{ P /\ b }}
              c1
                           {{ Q }}
            ELSE
                           {{ P /\ ~b }}
              c2
                           {{ Q }}
  
  
• loop:
  
                           {{ P }}
            WHILE b DO
                           {{ P /\ b }}
              c1
                           {{ P }}
            LOOP
                           {{ P /\ ~b }}
  
  
• consequence:
  
                           {{ P }} =>
                           {{ P' }}
            c
                           {{ Q }}
  
  (where P st implies P' st for all states st)
  
                           {{ P }}
            c
                           {{ Q' }} =>
                           {{ Q }}
  
  (where Q' st implies Q st for all states st)

A simple example:

                                 {{ True }} =>
                                 {{ x = x }}
    X ::= ANum x;
                                 {{ X = x }} =>
                                 {{ X = x /\ z = z }}
    Z ::= ANum z;
                                 {{ X = x /\ Z = z }} =>
                                 {{ Z - X = z - x }}
    WHILE BNot (!X === A0) DO
                                 {{ Z - X = z - x /\ X <> 0 }} =>
                                 {{ (Z - 1) - (X - 1) = z - x }}
      Z ::= !Z --- A1;
                                 {{ Z - (X - 1) = z - x }}
      X ::= !X --- A1
                                 {{ Z - X = z - x }}
    LOOP;
                                 {{ Z - X = z - x /\ ~ (X <> 0) }} =>
                                 {{ Z = z - x }} =>
                                 {{ Z + 1 = z - x + 1 }}
    Z ::= !Z + A1
                                 {{ Z = z - x + 1 }}

Exercise: hoare rules for 'repeat'

Exercise: 4 stars (hoare_repeat)

In this exercise, we've added a new construct to our language of commands: CRepeat. You will write the evaluation rule for repeat and add a new hoare logic theorem to the language for programs involving it.

We recommend that you do this exercise before the ones that follow - it should help solidify your understanding of the material.

repeat behaves like while, but the loop guard is checked after each execution of the body, with the loop repeating as long as the guard stays false. Because of this, the body will always execute at least once. The concrete syntax for CRepeat c b often looks like:

   repeat c until b

Add new rules for repeat to ceval below. You can use the rules for while as a guide, but remember that the body of a repeat should always execute at least once, and that the loop ends when the guard becomes true. Then update the ceval_cases tactic to handle these added cases.

A couple of definitions from above, copied so they use the new ceval.

Now state and prove a theorem, hoare_repeat, that expresses an appropriate proof rule for repeat commands. Use hoare_while as a model.

☐

Using Hoare Logic to reason about programs

Some miscellaneous lemmas for the examples

Formal Hoare-logic proofs often require a bunch of small algebraic facts, most of which we wouldn't even bother writing down in an informal proof. This is a bit clunky in Coq (though it can be made better using some of the automation features we haven't discussed yet). The best way to deal with it is to break them out as separate lemmas so that they don't clutter the main proofs. Here we collect a bunch of properties that we'll use in the examples below.

Exercise: Reduce to zero

A very simple while loop that needs no invariant:

A decorated version of this program, establishing a simple specification:

                                     {{ True }}
        WHILE BNot (!X === A0) DO
                                     {{ True /\ X <> 0 }} =>
                                     {{ True }}
          X ::= !X --- A1.
                                     {{ True }}
        LOOP
                                     {{ True /\ X = 0 }} =>
                                     {{ X = 0 }}

Your job: translate this proof to Coq. (It may help to look at the slow_subtraction proof below for ideas.)

Exercise: 2 stars (reduce_to_zero_correct)

☐

Example: Slow subtraction

The decorated program:

                                  {{ X = x /\ Z = z }} =>
                                  {{ Z - X = z - x }}
    WHILE BNot (!X === A0) DO
                                  {{ Z - X = z - x /\ X <> 0 }} =>
                                  {{ (Z - 1) - (X - 1) = z - x }}
      Z ::= !Z --- A1;
                                  {{ Z - (X - 1) = z - x }}
      X ::= !X --- A1
                                  {{ Z - X = z - x }}
    LOOP
                                  {{ Z - X = z - x /\ ~ (X <> 0) }} =>
                                  {{ Z = z - x }}

Here's another good use of the omega tactic.

Exercise: Slow addition

Your turn...

The following program adds the variable X into the variable Z by repeatedly decrementing X and incrementing Z.

Exercise: 3 stars (add_slowly_decoration)

Following the pattern of the subtract_slowly example above, pick a precondition and postcondition that give an appropriate specification of add_slowly, then decorate the program accordingly.

☐

Exercise: 3 stars (add_slowly_formal)

Now write down your specification of add_slowly as a Coq Hoare_triple and prove it valid.

☐

Example: Parity

Here's another, slightly trickier example. Make sure you understand the decorated program completely. (Understanding all the details of the Coq proof is not required, though it is not actually very hard -- all the required ideas are already in the informal version, and all the required miscellaneous facts about arithmetic are recorded above.)

This looks pretty awful until you just wave the omega wand.

Proof of correctness:

                               {{ X = x }} =>
                               {{ X = x /\ 0 = 0 }}
  Y ::= A0;
                               {{ X = x /\ Y = 0 }} =>
                               {{ (Y=0 <-> ev (x-X)) /\ X<=x }}
  WHILE BNot (!X === A0) DO
                               {{ (Y=0 <-> ev (x-X)) /\ X<=x /\ X<>0 }} =>
                               {{ (1-Y)=0 <-> ev (x-(X-1)) /\ X-1<=x }}
    Y ::= A1 --- !Y;
                               {{ Y=0 <-> ev (x-(X-1)) /\ X-1<=x }}
    X ::= !X --- A1
                               {{ Y=0 <-> ev (x-X) /\ X<=x }}
  LOOP
                               {{ (Y=0 <-> ev (x-X)) /\ X<=x /\ ~(X<>0) }} =>
                               {{ Y=0 <-> ev x }}

Exercise: 3 stars (wrong_find_parity_invariant)

My first attempt at stating an invariant for find_parity was the following.

Why didn't this work? (Hint: Don't waste time trying to answer this exercise by attempting a formal proof and seeing where it goes wrong. Just think about whether the loop body actually preserves the property.)

☐

Example: finding square roots

Exercise: 3 stars (sqrt_informal)

Write a decorated program corresponding to the above correctness proof.

☐

Exercise: Factorial

Recall the factorial Imp program:

Exercise: 4 stars (fact_informal)

Decorate the fact_com program to show that it satisfies the specification given by the pre and postconditions below. Just as we have done above, you may omit the algebraic reasoning about arithmetic, <=, etc., that is (formally) required by the rule of consequence:

(* FILL IN HERE *)


                               {{ X = x }}
  Z ::= !X;
  Y ::= ANum 1;
  WHILE BNot (!Z === A0) DO
    Y ::= !Y *** !Z;
    Z ::= !Z --- A1
  LOOP
                               {{ Y = real_fact x }}

☐

Exercise: 4 stars, optional (fact_formal)

Prove formally that fact_com satisfies this specification, using your informal proof as a guide. You may want to state the loop invariant separately (as we did in the examples).

☐