From leavens@cs.uiowa.edu Wed Mar 14 06:44:52 2001 MIME-Version: 1.0 Date: Wed, 14 Mar 2001 06:45:31 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: Homework 4 Content-Type: text/plain; charset=us-ascii Kevin, you wrote: > Trying to get a clue what to do for problem 1, I thought I would work > Cohen's problem 6.3 first. I'm not having much success. The way I am > approaching 6.3 is to start with > > H ==> ( P ==> Q ) > > Where: > H := (Y ==> Z) > P := ( X /\ Y ) > Q := ( X /\ Z) > > I would then be looking at: > > (Y ==> Z) ==> ( ( X /\ Y ) ==> ( X /\ Z) ) > > Since I have no way to introduce X if I start with just Y ==> Z, it looks > like I'll have to start with the whole thing and prove it true. > > That's what I've been trying to do. But I haven't had success. The best I > could get is > > X ==> ( Y ==> Z) > > The two questions I have at this point are: > > 1. Do you think that solving Cohen 6.3 will prove insightful for solving > problem 1 on homework 4? Cohen's 6.3 is essentially equivalent to problem 1 on homework 4. So if you can solve that, you will solve problem 1. > 2. If so, does the above approach to 6.3 look reasonable? Yes, I think that to prove this kind of thing my strategy would also be to reduce the entire thing to true. You are strarting at the right place. You might trying using the equivalence: P ==> (Q ==> R) <==> P /\ Q ==> R, which to me looks like it will help, although I'm not sure... Gary From leavens@cs.uiowa.edu Thu Mar 15 15:53:44 2001 MIME-Version: 1.0 Date: Thu, 15 Mar 2001 15:54:22 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: Solving for E - Another HW 4 Question Content-Type: text/plain; charset=us-ascii Kevin, You wrote: > I have a two questions: > > QUESTION 1 > > I understand that the proof for program > > {Q} S {R} > > Can be shortened to > > Q > > ==> wp.S.R> > > wp.S.R > > To use this form, is the hint simply "Hoare Triple" ? I'm not sure that you would have a single hint in this format, since in general there would be multiple steps. I think we would just take this as a valid proof outline that shows what you want to prove, and put in the hints the reasons for the individual steps along the way. > QUESTION 2 > > I'm looking at the example that starts at the bottom of page 111. > > The first step in solving for E begins with wp.S.R. The fact that the > precondition implies wp.S.R is not included in the derivation of E. > > Rather, the precondition is introduced only after we know the value of E. > Then the constraints of the precondition are used to simplify E. This seems > justified because it makes sense in the example, but the calculational > approach seems to have been short circuited. > > When I am solving for E can I follow this same pattern? Yes. Cohen first finds the value for E that makes wp.(a,q := a + c,E).(q == a * c) equivalent to true (since if you put the value of E in the bottom of the top calculation on page 112, that's what you get). This is in some sense the value of E that makes the weakest possible assumption. Then he's deriving a simpler value for E based on the precondition (a stronger assumption, since it implies true) in the second calculation on p. 112. This is always a valid way to proceed. I believe that you could also combine these two steps, but it looks clearer to separate them like this. Does that help? We'll talk about it on Tuesday also. Gary From leavens@cs.uiowa.edu Sat Mar 17 14:30:08 2001 MIME-Version: 1.0 Date: Sat, 17 Mar 2001 14:30:46 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Rex Gray Subject: Re: Homework 4a Content-Type: text/plain; charset=us-ascii Rex, you wrote: > I've found that I can solve question 1, but I haven't consciously used the > proof shapes described in chapter 6. We will make much more use of these in the coming chapters, because working with Hoare triples typically involves implications. > I haven't yet attempted the rest of the > exercises, so maybe I'll gain some insight from them, but please comment on > the following two statement/questions. > > 1. The use of implication in chapter 6 has shown me I don't have a handle on > its meaning. Implication is surely the trickiest logical operator, historically it gives everyone trouble... > On page 62, Cohen defines the meaning for implication as P ==> > Q is true, if either Q is true or P is false. In chapter 6, we seem to be > saying that since P is true, then Q is true also. I think what's going on is that, if we assume P ==> Q, then whenever P is true, the only possibility for Q that is consistent with the assumption is that Q is true. This is the usual, or everyday, meaning of implication, in that making P true makes Q true. > 2. On page 103, Cohen explains a way of viewing a calculation as H ==> ( P > op Q ). That is, a calculatoin of the form P op < hint H > Q is valid when H ==> (P op Q). Yes, that's right. > This seems confusing to me. One could not replace op with /\ or \/, > right? In fact, H looks like the operator to me. And, I'm not sure I > understand in what way <==>, ==>, <==, <=!=> are operators. Yes I agree we would never use /\ or \/ in place of op in such a calculation. The main reason is that they aren't transitive. That is, if we had several steps, like: P op < hint H0 > X op < hint H1> Q then if op were /\ (or \/), assuming H0 and H1 wouldn't allow us to conclude that P /\ Q (or P \/ Q). At least I don't see why we would However, we can use one of ==, <==>, ==>, or <==, because these are transitive. Similarly, we can't use <=!=> because it's not transitive. Good question! Does that help? We'll discuss this more on Tuesday... Gary From leavens@cs.uiowa.edu Sat Mar 17 15:52:30 2001 MIME-Version: 1.0 Date: Sat, 17 Mar 2001 15:53:07 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Rex Gray Subject: Re: Homework 4a, a minor correction to my earlier email Content-Type: text/plain; charset=us-ascii Rex, I wrote: > Yes I agree we would never use /\ or \/ in place of op in such a calculation. > The main reason is that they aren't transitive. That is, if we had several > steps, > like: > > P > op < hint H0 > > X > op < hint H1> > Q > > then if op were /\ (or \/), assuming H0 and H1 wouldn't allow us to conclude > that P /\ Q (or P \/ Q). Well, actually, conjunction (/\) *is* transitive, since if we have P /\ X and also X /\ Q, then P /\ Q follows. That is, P /\ X /\ X /\ Q ==> P /\ Q. Certainly, \/ isn't transitive, and neither is <=!=>, so I think that does explain why we can't use them in proof outlines as the operator. However, I don't know how to explain why we don't use /\ as the operator in a proof outline like this. There must be some reason. I guess that it's just an odd way to prove H0 /\ H1 ==> P /\ Q, since it seems more direct to use the outline: P /\ Q == < hint H0 > Z == < hint H1 > true The above outline also doesn't involve any extra work, since it's equivalent to what we set out to prove. One could also use two separate proofs of P and Q, and combine them, which I think would also be clearer than using /\ as the op. Perhaps (H0 ==> (P /\ X)) /\ (H1 ==> (X /\ Q)) ==> (H0 /\ H1 ==> P /\ Q) is invalid, which would be a more definitive reason, but I don't think it is. (That is, I think it's valid.) Anyway, this is fairly pedantic, and I hope it's not too confusing. Just wanted to correct my mistake... Gary From leavens@cs.uiowa.edu Mon Mar 19 13:04:12 2001 MIME-Version: 1.0 Date: Mon, 19 Mar 2001 13:03:37 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: One more HW 4 Question, question 6 Content-Type: text/plain; charset=us-ascii Kevin, you wrote: > I've been pondering homework question 6 (which proof of implication provides > something stronger than necessary?). > > Two possibilities are evident to me: > > 1. proofs that use equivalence rather than implication. > I don't think these really provide anything stronger since the forms > used are equivalent to implication. > > 2. proofs involving intermediary X. > The use of the intermediary isn't strictly necessary, so these seem to > be the ones we're looking for. > > I'm not confident I understand the question completely. Does my reasoning > above seem appropriate? Let me give an example, at the bottom of p. 101, Cohen says you can prove P ==> Q by a proof of the following form: P <==> P /\ Q This doesn't prove anything stronger than necessary, because what we're trying to prove, P ==> Q, is equivalent to P <==> P /\ Q. That is, P ==> Q <==> (P <==> P /\ Q). However, if we are trying to prove P ==> Q and we use a proof of the form P <==> Q then we have proved something stronger than necessary, since we have proved P <==> Q, and (P <==> Q) ==> (P ==> Q) but the converse doesn't hold. So if I understand you correctly, I think your alternative 1 is right. I think the intermediaries aren't relevant; they don't necessarily make what we're proving stronger than necessary or not. For example, we could prove P ==> Q by the outline: P <==> X <==>

Q and we'd be proving something stronger than necessary, because this is a proof of P <==> Q, still. Similarly, we could prove P ==> Q by the proof outline: P <==> X <==>

P /\ Q and we would be proving something equivalent to P ==> Q still. So the use of an intermediary doesn't matter. Does that help? Gary