From leavens@larch.cs.iastate.edu Mon Oct 25 16:54:11 2004 Date: Mon, 25 Oct 2004 16:54:11 -0500 (CDT) From: Gary T. Leavens To: Daniel Patanroi Subject: Re: composition Hi Dan, On Mon, 25 Oct 2004, Daniel Patanroi wrote: > Dr. Leavens. > > I have a question regarding composition of substitutions. > Looking at the example on your handout lambda-prolog-semantics.txt > at the end of page 7, > > why Q |-> Z is in the result > and why X |-> sue is not. Good point, that is a mistake. The domain of s' o s should be the same as the domain of s. So the example should be: {Q |-> Z, X |-> sue} o {Y |-> (foo X), R |-> bob} = {Y |-> (foo sue), R |-> bob} Thanks. > If s = {}, then s[[A]] = A ? Yes. > On the homework 4, should we read on a specific reading on any handouts > that you gave us? No, but reading the 2 excerpts from Hennessy's book I put in your box may be helpful. 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 daniel.patanroi@gmail.com Fri Oct 29 16:41:53 2004 Date: Fri, 29 Oct 2004 16:41:44 -0500 From: Daniel Patanroi To: Gary T. Leavens Subject: hw4 Dr. Leavens, For Adding Boolean problem, do you want the following signature lt int -> int -> expression. equals value -> value -> expression. OR lt expression -> expression -> expression. equals expression -> expression -> expression. Of course, for the 2nd option, I will make sure that lt works only for (num I) and equals only works for (num I) or (bool B). The second question, and E1 E2 should work only with boolean, right? Thus, and (num 1) (num 1) should not work ? Please kindly explain. Dan From leavens@larch.cs.iastate.edu Sat Oct 30 00:07:26 2004 Date: Sat, 30 Oct 2004 00:07:25 -0500 (CDT) From: Gary T. Leavens To: Daniel Patanroi Subject: Re: hw4 environment problem Hi Daniel, On Fri, 29 Oct 2004, Daniel Patanroi wrote: > Thanks for replying so quick. > I have another question on the last problem. > > I don't quite see how to use predicate 'test-env'. > > Right now I embed the environment directly on while_test_helper_env.mod > So I have something like below: > > runC I LS :- testC I C, meaningC (bind "1" 1) C STO, > show_store 0 STO LS. > > And that works just fine. > > Is it okay? Or do I miss something here? You can use test_env as in in the same way that meaningC uses init_store. For example, test_env Env will unify Env with whatever the definition of test_env says. 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 Nov 1 00:58:14 2004 Date: Mon, 1 Nov 2004 00:58:14 -0600 (CST) From: Gary T. Leavens To: Neeraj Khanolkar Subject: Re: Expression test for inc? Hi Neeraj, The expression tests use an initial store with the value three stored in location one. See the definition of runE %% ``runE I V S'' succeeds if the Ith test, run on a store where %% location 1 is set to 3, produces the value V and store S. runE I V S :- testE I E, initial_store S0, (update S0 1 3 S1), meaningE E S1 V S. On Sun, 31 Oct 2004, Neeraj Khanolkar wrote: > > Hi Gary, > > For some reason the following expression test for inc fails: > > testcaseE 5 (inc (loc 3)) 1 (0::0::0::1::nil). > > is it because of the way the initial store is created for the expression > tests? When I control the creation of the initial store using a command > test, it succeeds. For example this command test works fine: > > testcaseC 8 (semi > (semi > (assign (loc 5) (num 4) ) > (exp (inc (loc 5)) ) > ) > (assign (loc 4) (inc (loc 5)) ) > ) > (0::0::0::0::5::6::nil). > > Inc seems to be implemented correctly, since the above test fails on > alteration of the list (final store). That because the testing for commands does not use an initial store with any values in it originally. 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 Nov 1 01:03:38 2004 Date: Mon, 1 Nov 2004 01:03:38 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Sun, 31 Oct 2004 rhe@cs.iastate.edu wrote: > How are you going? Fine thanks. > I have some questions in homework 4. Could you be kind enough to answer them? Of course. > 1. For Question 6. Are we supposed to define intval and boolval as follow? > > type intval int -> value. > type boolval boolean -> value. I don't normally answer questions about whether answers are exactly correct or not.but I don't see any particular problems with this one. :-) > 2. For Question 6. > For *lt*. In which way are we supposed to define it? > > type lt expression -> expression -> boolean. > > or > > type lt expression -> expression -> expression. > > or > > type lt expression -> expression -> boolean -> o. > > In your requirement, it is said that *lt E1 E2* only works for integer arguemnts > and returns a boolean. lt E1 E2 is supposed to be an expression; that should tell you the return type. The computation is done by the semantics, not by the expression itself. > If the argument expression is not integer, > how do we need to do? Just leave it alone or add some type checking? You can just let it get 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 ----------------------------------------------- From leavens@larch.cs.iastate.edu Tue Nov 2 01:23:09 2004 Date: Tue, 2 Nov 2004 01:23:09 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Mon, 1 Nov 2004 rhe@cs.iastate.edu wrote: > Dear Professor: > > Thank you for your quick response. > > Could you be kind enough to answer the following question: > > When we do Problem 6, are we also supposed to update the solution code for > Problem 1 and 3? It means that the problem 6 need to cover the case of *inc* > and *do*. Yes, that's right. 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 Nov 2 20:06:33 2004 Date: Tue, 2 Nov 2004 20:06:33 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Tue, 2 Nov 2004 rhe@cs.iastate.edu wrote: > Dear Professor: > > Could you be kind enough to answer the following question? > > Initially, *access0 S L V* returns 0 if there was no value stored at L. > > When updated for the value type, do I need to specify two values if there was no > value stored at L, > one is for (intval 0) and the other is for (boolval ff)? > Or just (intval 0) is enough? I think just having access0 return (intval 0) when nothing has been stored in a given location is fine. 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 Thu Nov 4 02:17:25 2004 Date: Thu, 4 Nov 2004 02:17:25 -0600 (CST) From: Gary T. Leavens To: Raul Piaggio Subject: Re: Question about HW 4 - Ex. 5 Hi Raul, On Tue, 2 Nov 2004, Raul Piaggio wrote: > I hope your travel is going well. I have a question about the last exercise, > the one about environments. Thanks, it's been an interesting conference so far. > Since the environment is not part of the configuration (and with the > signature given for the reduction predicates), I don't find a way to return > an environment from a reduction if the environment if modified during the > reduction. This can happen when we make an assignment to a location with a > new name, and we do an overlay on the environment. Environments are not supposed to be modified during reductions. The environment is fixed and unchanging during executions of commands and expressions. You would only make assignments to locations with existing names. This does not allow for "declaration commands" which are a future of C++ and Java. However, its normal to separate declarations into a separate syntactic category, so we are not considering them to be part of commands or expressions. > The possible ways out I see are: making the environment part of the > enviorment, or only use predetermined names (maybe this is why we need that > test_env, now that I think of it). > > Could you please confirm if we are supposed to use only predetermined name > bindings during execution? Yes, that's correct. 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 Thu Nov 4 02:24:50 2004 Date: Thu, 4 Nov 2004 02:24:49 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Wed, 3 Nov 2004 rhe@cs.iastate.edu wrote: > How are you? Thank you for your quick response. Fine thanks. > Could you be kind enough to answer my following question in Homwork 4? Sure. > For the Question 7 (last question): Which version of code am I supposed to > update? > My update is based on the original one downloaded from your website? > Or the code updated for question 1 and 3, which includes the *inc* and *do*? > Or the code updated for question 6, which includes the *value* ? I would prefer you worked from the code updated from question number 6. 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 Thu Nov 4 02:26:12 2004 Date: Thu, 4 Nov 2004 02:26:12 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Wed, 3 Nov 2004 rhe@cs.iastate.edu wrote: > Dear Professor: > > How are you? I am sorry that I have another question in last problem. > > Could you be kind enough to answer it? Sure, > When *id* is added, is *loc 2* still allowed to be a legal expression in the > system or not? You can still allow loc 2 as a kind of location in the language. > If it is allowed, then I could use both *loc* and *id* to specify a location. Yes. 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 Thu Nov 4 21:47:53 2004 Date: Thu, 4 Nov 2004 21:47:53 -0600 (CST) From: Gary T. Leavens To: rhe@cs.iastate.edu Subject: Re: Some questions in homework 4 Hi Ru, On Thu, 4 Nov 2004 rhe@cs.iastate.edu wrote: > Thank you for your guidance. > > Could you be kind enough to answer my following questions? > > 1. For the relation of *accumulate*. > For your code, while_test accumulate while_test_helpers. > (Of course, while_test_helpers do not accumulate while_test.) > > Since testCaseC is declared in while_test_helpers.sig, > while_test_helpers.mod know the type of testCaseC. Yes, while_test_helpers knows the type of testcaseC. > But the concrete facts of testCaseC is defined in while_test.mod, > while_test_helpers.mod does not accumulate while_test.mod so that > while_test_helpers.mod should be unable to reach the concrete facts of testCaseC > in while_test.mod, > then why could *runC 3 L* still work fine? Because it is run in while_test. > 2. For question 7. When you suggest us to introduce test_env, > you say that the rules for test_env should go in the while_test_env. > Where should I put the declaration of test_env? In while_test_helpers_env.sig? Yes, I think so. > 3. Do you want the enviroment argument is added in *testcaseC*? No, I used test_env in the definition of runC. > Or we can assume that there is only one enviroment for all the *testcaseC* > so that we do not need enviroment as the argument of *testcaseC*? Yes, that's effectively what I did. 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 Thu Nov 4 22:02:11 2004 Date: Thu, 4 Nov 2004 22:02:11 -0600 (CST) From: Gary T. Leavens To: Neeraj Khanolkar Subject: Re: development forks Hi Neeraj, On Thu, 4 Nov 2004, Neeraj Khanolkar wrote: > > Hi Gary, > > Sorry for such a basic question but I wanted to wrap this up tonight. > > I've modified incrementally, the orignal files (your files) for questions > 1, 3 and 4. > For question 6 I went back again to the original files and modified. > For question 7 also back to the original files, renamed and modified. > > So for each of these 3 forks, I'll turnin a seperate printout. > Is this OK? Yes, I prefer to see a separate printout for various stages. But I'd prefer that 6 built on all of the previous problems and that 7 also builds on the previous problems. 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 ----------------------------------------------