From leavens@larch.cs.iastate.edu Thu Feb 23 11:44:49 2006 Date: Thu, 23 Feb 2006 11:44:49 -0600 (CST) From: Gary T. Leavens To: Kristina Boysen Subject: RE: problem 4 on HW 3 Hi Kristina, On Thu, 23 Feb 2006, Kristina Boysen wrote: >> Homework 3 in 641 is now available from the web page or directly from: >> >> http://www.cs.iastate.edu/~cs641/homework/hw3-dataflow.pdf >> >> You should already be able to do much of it... > Excellent, I can start work on it. Good :-) > So on problem 4 part a, if we are assuming that AExp* is empty and we iterate > through our example, do we add to it when an expression is in the gen set or > just when we find it? For example, if we have [i := i+1], i+1 would not be in > the gen set, but it would be a new AExp. You shouldn't assume that AExp* is empty, just that the iteration starts with {}. That doesn't change the set of nontrivial expressions that occur in the program (AExp*). This also doesn't change the genAE set, contrary to your example. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@larch.cs.iastate.edu Tue Feb 28 23:45:18 2006 Date: Tue, 28 Feb 2006 23:45:18 -0600 (CST) From: Gary T. Leavens To: Robert Dyer Subject: Re: CS641 HW3 Hi Robert, On Tue, 28 Feb 2006, Robert Dyer wrote: > Do you want us to show (in the calculational style) our computations > for the chaotic iteration algorithm in problem 6 (2.2)? It is simple > enough I can calculate it in a table rather quick, but this won't show > my actual calculations. If the calculational style isn't helpful for that, then you don't have to use that style. But if it makes things clearer and isn't too long, then try it out. > Also for problem 9 (mini project 2.1 part 1), I am a little confused > as to which two functions I am proving are equivalent. Am I proving > ud = du? No, those aren't the same. You are proving the specified/abstract function ud = UD (the one defined constructively). Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ----------------------------- From leavens@larch.cs.iastate.edu Mon Mar 20 03:04:25 2006 Date: Mon, 20 Mar 2006 03:04:25 -0600 (CST) From: Gary T. Leavens To: yecui@cs.iastate.edu Subject: Re: questions on hw Hi Cui, On Sun, 19 Mar 2006 yecui@cs.iastate.edu wrote: > I have some questions on homework. > > 1. Consider the following two rules. > < [return]^l, sigma > -> sigma > < [return]^l; S, sigma > -> sigma > Can I say that the first rule tells if [return]^l is the last statement, > then terminate, and the second one says if [return]^l is not the last statement, > then simply skip all the statements after it? No. You will have to change the sequencing rules to prevent interpretations that you do not want. Technically rules can be applied whenever they match the configuration. > My concern is in the case of < [return]^l; S, sigma >, whether we could > apply the first rule, which results in and which is not what > we want. Right. > I just want to make sure that the two rules above clearly seperate the > two cases without any ambiguity. No, they do not. > 2. Can we assume that there must be throw statement in try-catch statement? > By which I mean there will not be any try-catch statement that has no throw > in it. I would prefer that you not make that assumption, but you can if necessary. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ------------------------------ From leavens@larch.cs.iastate.edu Sat Mar 25 19:11:06 2006 Date: Sat, 25 Mar 2006 19:11:06 -0600 (CST) From: Gary T. Leavens To: yecui@cs.iastate.edu Subject: Re: question about mini project 2.22 for homework Hi Cui, On Wed, 22 Mar 2006 yecui@cs.iastate.edu wrote: > Also, a question in homework. In mini project 2.2, because the > proof of 2.22' is very similar to 2.21', could we just write > something similar to the book ("The proof is by induction on > the length of the derivation sequence and uses Theorem 2.21") > without writing the induction proof at all? Yes, for the part of mini-project 2.2 that requires you to state and prove something like Corollary 2.22 in the book, it's fine to just state the altered version of 2.22 and to say something similar to what is said for the book's proof of 2.22. The interesting bit is in the proof of 2.21. Sorry I couldn't answer this when I was away... Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------------------- From leavens@larch.cs.iastate.edu Tue Mar 28 20:54:19 2006 Date: Tue, 28 Mar 2006 20:54:19 -0600 (CST) From: Gary T. Leavens To: "Jing(Janet) Liu" Subject: Re: a question about homework 3.2 Hi Janet, On Tue, 28 Mar 2006, Jing(Janet) Liu wrote: > For the second part of Mini Project 2.1 where we have to "start from the > definition of du, develop an equantional definition of DU and verify its > correctness", could I use the following information given in the book without > proof? > $du(x,\ell) = \{(\ell^{'} | \ell \in ud(x,\ell^{'})\}$ Yes. > Also, for the requirement of verifying its correctness, are we supposed to do > something similar to "correctness of Live Variable Analysis" in section 2.2 > (which I guess not), or just simply prove that the DU definition we created is > equivalent as du (similar to the first part of Mini Project 2.1)? If it's the > latter case, then I can assert the correctness by saying that the equivalence > property is preserved during every step of the construction of DU from du, > right? I understood this as proving equivalence of DU and du, as in the first part of Mini Project 2.1 (the first alternative). Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------------------- From leavens@larch.cs.iastate.edu Wed Apr 5 23:36:41 2006 Date: Wed, 5 Apr 2006 23:36:41 -0500 (CDT) From: Gary T. Leavens To: Robert Dyer Subject: Re: CS641 question Hi Robert, On Wed, 5 Apr 2006, Robert Dyer wrote: > I was wondering about part(s) of question 11 from HW3. The definition > of [return] states it 'simply halts execution without changing the > state' and the definition of [assume] states 'to refuse to execute if > b is not true.' > > Am I right to assume those statements are somewhat equivalent? Or is > there a difference between refusing to execute and halting execution? > To me those sound the same. If they are different, how so? Is there > some simple example to show this difference? They are different. Refusing to execute, i.e., getting "stuck", is quite different than halting execution. If we have [x := 3]^1; [return]^2; [x := 4]^3 then the final state maps x to 3, but there is a final state. However, [x := 3]^1; [assume false]^2; [x := 4]^3 has no final state and is stuck. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 --------------------