From leavens@cs.uiowa.edu Sun Mar 25 11:31:29 2001 MIME-Version: 1.0 Date: Sun, 25 Mar 2001 11:31:53 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Elise Anderson Subject: Re: Chap 8 Content-Type: text/plain; charset=us-ascii Elise, you wrote: > Hi prof leavens, > > Did you every get the chance to see how the "do" loop > was expanded when using it in a proof? It looks like > that may be needed in this homework. I have not read > Chap 9, yet. So it may be in there. I'm not exactly sure what you mean by "expanding" a "do" loop in a proof. There are some examples of annotations of do loops in chapter 9. For example, look at section 9.1. In essence to do a proof of correctness for a do loop, you use the invariance theorem, much in the same way we used the if-theorem in the previous chapter. Gary From leavens@cs.uiowa.edu Tue Mar 27 22:20:56 2001 MIME-Version: 1.0 Date: Tue, 27 Mar 2001 22:21:39 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Timothy VanFosson Subject: Re: HW5, problem 10 Content-Type: text/plain; charset=us-ascii Timothy, Timothy VanFosson wrote: > I thought I had this solved, but when I took another look I found that my > solution did not satisfy d >= 1 as part of the invariant. In trying to > work through this I'm not sure how I can establish both d >= 1 and d * y <= > r since this would imply that the remainder is equal to or larger than the > divisor, which is clearly not what we want. I think it would work easily > if we let d >= 0 or if I can add a statement after the portion of code > after the do loop that removes the last "y" from r. I'm trying to solve this myself, but I think that you establish d*y <= r by the inner loop, since it's the negation of the inner loop's guard. Note that at the end of the inner loop, we end of with d and dd satisfying the same assertion (PP) that was true in the program developed by Cohen, so that the assignment r,q := r-dd, q+d should adjust q and r appropriately. That is, on the bottom of p. 147, we are just replacing the inner do loop. So I think that this assignment, r,q := r-dd, q+d, may be the one you want to use. In any case I'm sure you can't relax R0: 1 <= d to 0 <= d. Let me know if this helps... Gary From leavens@cs.uiowa.edu Wed Mar 28 12:03:46 2001 MIME-Version: 1.0 Date: Wed, 28 Mar 2001 12:04:32 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Timothy VanFosson Subject: Re: HW5, problem 10 Content-Type: text/plain; charset=us-ascii Tim, you wrote: > >What does shift(i) do? I presume divides by 2? > > Yes. Shift right or divide by 2. Good, that's what I thought. > I'm not sure what you mean by the placement of the code for q and r. This > is what I was working from: > > {P} > ;SS0 > {P /\ PP: (R0: 1 <= d) /\ (R2: dd = d * y)} > ;do d * y > r --> SS od > {P /\ PP /\ ~(d * y > r), hence P R0 R1 R2} > > Seemed to me that the code for q and r needed to go into SS. No, I think this is where your confusion is. I believe it can be made to work, actually as stated, without having to make a change to R0, if you put the statement r,q := r-dd, q+d after the code above, since it needs as a precondition P /\ R0 /\ R1 /\ R2. Don't assign to r and q in the loop (at all). > >What's your bound function for the inner loop? I guess either d or dd > >works... > > I hadn't gotten that far, but I think it ought to be d or dd - y. They > amount to the same thing. Hm, I get dd-r for the bound of the inner loop. Also, for bounding the outer loop, you really need to have d be positive (greater than or equal to 1) since otherwise the outer loop might not make progress. Gary From leavens@cs.uiowa.edu Wed Mar 28 13:20:55 2001 MIME-Version: 1.0 Date: Wed, 28 Mar 2001 13:21:41 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: 22C:181 Homework 5, problem 9 Content-Type: text/plain; charset=us-ascii Kevin, Kevin Lillis wrote: > Gary, > > I'm working on formalizing my own piece of code (homework problem 9) > > The code I chose to use determines the smallest value from an array of > non-negative integers. Therefore, every single array element needs to be > examined. > > It looks like the bound function will then involve only a counter and not > the deleted conjunct. > > Could it be that I have selected an inappropriate piece of code? Yes for demonstrating the technique in chapter 9, this isn't the right piece of code. You actually have an example appropriate for chapter 10, I think... Gary From leavens@cs.uiowa.edu Fri Mar 30 18:00:38 2001 MIME-Version: 1.0 Date: Fri, 30 Mar 2001 18:01:22 -0600 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: homework 3, problem 3 Content-Type: text/plain; charset=us-ascii Kevin, Kevin Lillis wrote: > I've been re-working the homework and have a question. > Homework #3 question #3 (Cohen's 4.2.c) reads: > > Specify a program that, given a boolean array b containing > at least one true, sets integer x to the smallest z such > that b.z holds. > > My original solution was > > var b : array of bool {EXISTS i : 0 <= i < #b : b.i <==> true} > ;var x : int > ;x : x = (MIN z : 0 <= z < #b /\ b.z <==> true : z) > > When I reworked the problem I came up with a different solution: > > var b : array of bool {EXISTS I : 0 <= i <#b : b.i <==> true} > ;var x : int > ;x : (FORALL z : 0 <= z < x : b.z <==> false) /\ b.x <==> true > > Is the second solution correct? It looks correct, but the English > specification has the words "sets integer x to" and my second solution > doesn't "set x" to a value as clearly as does my first solution. (in both, you need parentheses around the quantified expressions, and in the second the "I" should be "i".) Neither of them actually has an assignment to x in the postcondition. The form of the first gives the final value of x directly, while the form of the second gives it indirectly. So both are correct. I think I prefer the first, because it is somewhat shorter, and more direct. But the second has the advantage of looking more like linear search. You can shorten both by changing "b.x <==> true" to "b.x". Gary