From leavens@cs.uiowa.edu  Mon Feb 12 16:03:54 2001
MIME-Version: 1.0
Date: Mon, 12 Feb 2001 16:04:24 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Kevin Lillis <klillis@saunix.sau.edu>
Subject: Re: Homework 2
Content-Type: text/plain; charset=us-ascii

Kevin,

you wrote:

> I have worked on homework 2 all day Friday and most of the weekend and I'm
> having trouble completing the proofs involving implication.  Number 2, which
> is
>
> true ==> X <==> X
>
> is the only proof involving implication that I have been able to figure out.
>
> I've been working the proofs given in the text as they appear.  The examples
> given in the book seem straightforward.  When I attempt the problems
> assigned, however, I am stymied.  It seems that no matter which rules I
> apply, my proofs go nowhere.
>
> Any guidance or suggestions would help greatly.

Hmm, have you tried expanding the implications involved using the definition on
p. 34, or the lemma at the top of p. 35?  Be careful to get the precedence right
before working on either side, it may help to fully parenthesize the formulas
first.  Another idea is to start with the side of the formula that doesn't have
the implication  in it (if there is one).

Failing that, come to my office hours, or just come to class and we can discuss
it; the homework is a bit ahead of what we have talked about in class anyway...

    Gary


From leavens@cs.uiowa.edu  Mon Feb 12 17:26:06 2001
MIME-Version: 1.0
Date: Mon, 12 Feb 2001 17:26:47 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Kevin Lillis <klillis@saunix.sau.edu>
Subject: Re: Homework 2
Content-Type: text/plain; charset=us-ascii

Kevin,

Another hint, you may want to use the golden rule a fair bit, to convert between
conjunctions and implications, after you expand out one of the two formulas I
mentioned for implication.  Using the definition on p. 34 for implication is
often convenient, because disjunction distributes over equivalence...

    Gary


From leavens@cs.uiowa.edu  Mon Feb 12 21:48:07 2001
MIME-Version: 1.0
Date: Mon, 12 Feb 2001 21:48:47 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Elise Anderson <fbtigg@yahoo.com>
CC: Shu Liu <sliu@cs.uiowa.edu>
Subject: Re: negation
Content-Type: text/plain; charset=us-ascii

Elise

Elise Anderson wrote:

> Hi Prof Leavens and TA Liu,
>
> If I obtain "P V -P" while working out a proof, it
> evaluates to true, correct?

Yes, that's what the postulate called "Excluded Middle" says.  So it's
fine to replace P \/ !P with true.  It's slightly confusing because the
postulate isn't written as
     P \/ !P <==> true
but recall that the form given is equivalent:

        P \/ !P
<==>    <true is the unit of equivalence>
        P \/ !P <==> true

    Gary


From leavens@cs.uiowa.edu  Wed Feb 21 10:17:00 2001
MIME-Version: 1.0
Date: Wed, 21 Feb 2001 10:17:33 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Young Ki Kim <ykkim@cbucc.chungbuk.ac.kr>
Subject: The term "quantifier"
Content-Type: text/plain; charset=us-ascii

Young Ki,

You asked about the origin of the word "quantifier".  A mathetician
friend, Don Pigozzi, at Iowa State writes:

"I'm pretty sure that the term (in German) is due to Frege. Church's
book (my main quick source of information of this kind) doesn't say
anything about the origin of the term. It's entomology must be the
same as that of "quantity", which is latin. Webster's New Collegiate
Dictionary defines "quantifier" as "a prefixed operator that binds the
variables in a logical formula by specifying their quantity"--
everything in case of the universal quantifier and at least one in the
existential case."

Hope that helps,

    Gary

From leavens@cs.uiowa.edu  Wed Feb 28 11:19:42 2001
MIME-Version: 1.0
Date: Wed, 28 Feb 2001 11:20:22 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Kevin Lillis <klillis@sau.edu>
CC: Shu, Liu
Subject: Re: format for specifications
Content-Type: text/plain; charset=us-ascii

Kevin
you wrote:

> So far the examples of specifications have had only a single equation
> following the declarations.  Is it also acceptable to have multiple
> equations?  For example, one equation could assign to a variable X the value
> of the largest element in an array.  Subsequent equations could then simply
> reference X in lieu of providing the complete formula that obtained this
> value.

The grammar for specifications only permits one postcondition formula.
Unlike programming, you don't get to use assignment within specifications.
That is, there is only one state that you are describing (the post-state),
in the postcondition not a series of states (as you do in a sequential program).

However, you can, within the single postcondition, of course, use conjunctions,
which allow you to break apart what you want to specify for the post-state into
several parts.

Finally, if you want to give a name to something, like the largest value
in an array, you can either use a ghost variable, or you can use a function
that you name and refer to in several places.  See, the solution I sent out
yesterday for the second-largest element specification for an example.

    Gary


From leavens@cs.uiowa.edu  Mon Mar  5 16:39:00 2001
MIME-Version: 1.0
Date: Mon, 05 Mar 2001 16:39:01 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Kevin Lillis <klillis@saunix.sau.edu>
CC: leavens@cs.iastate.edu
Subject: Re: Proving Statements Equal
Content-Type: text/plain; charset=us-ascii

Kevin,

you wrote:

> When proving two statements S and T are equal
>
> do I need to show
>
>         {Q} S {P} <==> {Q} T {R}
>
> or can I simply show
>
>         wp.S.R <==> wp.T.R

According to the definition of program equivalence (p. 86), the latter
suffices, if you do it for an arbitrary R.

    Gary

From leavens@cs.uiowa.edu  Mon Mar  5 16:49:26 2001
MIME-Version: 1.0
Date: Mon, 05 Mar 2001 16:49:29 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: Timothy VanFosson <timv@ccad.uiowa.edu>
CC: leavens@cs.iastate.edu
Subject: Re: HW 3, problem 17
Content-Type: text/plain; charset=us-ascii

Tim,

you wrote:

> I'm struggling with problem 17, the proof of 5.10, which is that an empty
> do is replaceable by skip.  In particular, I'm not sure what form the proof
> needs to take and I'm not sure what "replaceable" means.  By replaceable do
> we mean "equivalent" or that an empty do implies skip?  Since he never
> defines wp.S for do, I'm not sure how to proceed to prove equivalence
> (other than by mutual implication).  Any hints you can give me?

Good questions.  By "replaceable", Cohen may mean "equivalent",
but as you note, I don't see how to prove that, because we haven't been
given the wp defininition of the repitition yet.  So I guess he must be
thinking
that "replaceable" means refinement, that is, that "skip" refines "do od",
in the sense that wp.(do od).R <== wp.skip.R.

I think you can use the refinement definition and the invariance theorem (p.
99's version!) to do the proof.  We'll discuss it in class...

    Gary

From leavens@cs.uiowa.edu  Tue Mar  6 22:55:20 2001
MIME-Version: 1.0
Date: Tue, 06 Mar 2001 22:55:53 -0600
From: "Gary T. Leavens" <leavens@cs.uiowa.edu>
Reply-To: leavens@cs.uiowa.edu
X-Accept-Language: en,de,fr
To: leavens@cs.iastate.edu
CC: Gary Leavens <leavens@cs.uiowa.edu>, Shu Liu <sliu@cs.uiowa.edu>,
        Students in 181 <c181@cs.uiowa.edu>,
        Timothy VanFosson <timv@ccad.uiowa.edu>,
        Jeff Mohror <jmohror@nads-sc.uiowa.edu>,
        Kevin Lillis <klillis@saunix.sau.edu>, Shrisha Rao <srao@cs.uiowa.edu>,
        Young Ki Kim <ykkim@cbucc.chungbuk.ac.kr>
Subject: Re: HW 3, refinement (problem 17) and Hoare triples vs. wp for equality
Content-Type: multipart/mixed;
 boundary="------------53FCED56C8AC4F832DBFEAB1"

Hi,

I said in class today that my email remarks (also on the Q & A pages)
about refinement were wrong.  I have always had a hard time with
the direction of this, and there I made the mistake of thinking I had
made a mistake.  That is, when I said...

> ... that "replaceable" means refinement, that is, that "skip" refines "do od",
> in the sense that wp.(do od).R <== wp.skip.R.

This was correct, despite what I said in class.  Sorry for the confusion.

Another thing that came up in class today was Jeff's proof of problem 10,
in which he proved that (S;skip) == skip, by showing, for all Q and R,
that {Q} S;skip {R} <==> {Q} skip {R}.  This doesn't use the definition
of program equivalence on p. 86, which would show that
  wp.(S;skip).R == wp.skip.R
for all R.  However, I wondered if it was a valid proof principle.  It turns out
that it is an equivalent way to prove the equivalence of programs with our
definitions.  This is shown in the attached file.

    Gary
			 Notes on Homework 3
			  by Gary T. Leavens
		     $Date: 2001/03/07 04:54:37 $
				   
Lemma: To prove equality of statements, it is necessary and sufficient
      to prove that they have the same Hoare triple annotations.  That is,
      for all statements, S, T,
          (\forall P, Q : : {P} S {Q} <==> {P} T {Q}) <==> (S == T)

Proof: Let S and T be given.  We proceed by mutual implication.

    For the forward direction, we calculate as follows.
      
    (\forall P, Q : : {P} S {Q} <==> {P} T {Q})
<==>   <definition of Hoare triple>
    (\forall P, Q : : (P ==> wp.S.Q) <==> (P ==> wp.T.Q))
<==>   <impl, twice, with a view towards getting the wp's together>
    (\forall P, Q : : (P \/ wp.S.Q) <==> wp.S.Q <==> (P \/ wp.T.Q) <==> wp.T.Q)
<==>   <associativity and symmetry>
    (\forall P, Q : : (P \/ wp.S.Q) <==> (P \/ wp.T.Q) <==> wp.S.Q <==> wp.T.Q)
<==>   <disjunction distributes over equivalence>
    (\forall P, Q : : (P \/ (wp.S.Q <==> wp.T.Q)) <==> wp.S.Q <==> wp.T.Q)
<==>   <impl>
    (\forall P, Q : : P ==> (wp.S.Q <==> wp.T.Q))
 ==>   <instantiation, with P := true, since P does not figure in equality>
    (\forall Q : : true ==> (wp.S.Q <==> wp.T.Q))
<==>   <predicate calculus>
    (\forall Q : : wp.S.Q <==> wp.T.Q)
<==>   <definition of program equality>
    S == T

    For the other direction, assume that S == T, i.e.,
    that (\forall Q : : wp.S.Q <==> wp.T.Q).  As shown in Cohen's chapter 6,
    proving that (\forall P, Q : : {P} S {Q} <==> {P} T {Q})
    under this assumption is the same as proving the implication we need.
    So let P and Q be given.  We can calcluate as follows.

     {P} S {Q}
<==>   <definition of Hoare triple>
     P ==> wp.S.Q
<==>   <by assumption, wp.S.Q <==> wp.T.Q>
     P ==> wp.T.Q
<==>   <definition of Hoare triple>
     {P} T {Q}
 -=- MIME -=- 
This is a multi-part message in MIME format.
--------------53FCED56C8AC4F832DBFEAB1
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

Hi,

I said in class today that my email remarks (also on the Q & A pages)
about refinement were wrong.  I have always had a hard time with
the direction of this, and there I made the mistake of thinking I had
made a mistake.  That is, when I said...

> ... that "replaceable" means refinement, that is, that "skip" refines "do od",
> in the sense that wp.(do od).R <== wp.skip.R.

This was correct, despite what I said in class.  Sorry for the confusion.

Another thing that came up in class today was Jeff's proof of problem 10,
in which he proved that (S;skip) == skip, by showing, for all Q and R,
that {Q} S;skip {R} <==> {Q} skip {R}.  This doesn't use the definition
of program equivalence on p. 86, which would show that
  wp.(S;skip).R == wp.skip.R
for all R.  However, I wondered if it was a valid proof principle.  It turns out
that it is an equivalent way to prove the equivalence of programs with our
definitions.  This is shown in the attached file.

    Gary

--------------53FCED56C8AC4F832DBFEAB1
Content-Type: text/plain; charset=us-ascii;
 name="hw3-notes.txt"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
 filename="hw3-notes.txt"

			 Notes on Homework 3
			  by Gary T. Leavens
		     $Date: 2001/03/07 04:54:37 $
				   
Lemma: To prove equality of statements, it is necessary and sufficient
      to prove that they have the same Hoare triple annotations.  That is,
      for all statements, S, T,
          (\forall P, Q : : {P} S {Q} <==> {P} T {Q}) <==> (S == T)

Proof: Let S and T be given.  We proceed by mutual implication.

    For the forward direction, we calculate as follows.
      
    (\forall P, Q : : {P} S {Q} <==> {P} T {Q})
<==>   <definition of Hoare triple>
    (\forall P, Q : : (P ==> wp.S.Q) <==> (P ==> wp.T.Q))
<==>   <impl, twice, with a view towards getting the wp's together>
    (\forall P, Q : : (P \/ wp.S.Q) <==> wp.S.Q <==> (P \/ wp.T.Q) <==> wp.T.Q)
<==>   <associativity and symmetry>
    (\forall P, Q : : (P \/ wp.S.Q) <==> (P \/ wp.T.Q) <==> wp.S.Q <==> wp.T.Q)
<==>   <disjunction distributes over equivalence>
    (\forall P, Q : : (P \/ (wp.S.Q <==> wp.T.Q)) <==> wp.S.Q <==> wp.T.Q)
<==>   <impl>
    (\forall P, Q : : P ==> (wp.S.Q <==> wp.T.Q))
 ==>   <instantiation, with P := true, since P does not figure in equality>
    (\forall Q : : true ==> (wp.S.Q <==> wp.T.Q))
<==>   <predicate calculus>
    (\forall Q : : wp.S.Q <==> wp.T.Q)
<==>   <definition of program equality>
    S == T

    For the other direction, assume that S == T, i.e.,
    that (\forall Q : : wp.S.Q <==> wp.T.Q).  As shown in Cohen's chapter 6,
    proving that (\forall P, Q : : {P} S {Q} <==> {P} T {Q})
    under this assumption is the same as proving the implication we need.
    So let P and Q be given.  We can calcluate as follows.

     {P} S {Q}
<==>   <definition of Hoare triple>
     P ==> wp.S.Q
<==>   <by assumption, wp.S.Q <==> wp.T.Q>
     P ==> wp.T.Q
<==>   <definition of Hoare triple>
     {P} T {Q}

--------------53FCED56C8AC4F832DBFEAB1--