Darren New wrote:
> Chris Smith wrote:
>> Specialized
>> language already exist that reliably (as in, all the time) move array
>> bounds checking to compile time;
>
> It sounds like this means the programmer has to code up what it means to
> index off an array, yes? Otherwise, I can't imagine how
Joachim Durchholz wrote:
> Marshall schrieb:
> > Chris Smith wrote:
> >> Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> >> I *think* I understand Marshall here. When you are saying "assignment",
> >> you mean assignment to values of attributes within tuples of the cell.
> >> When Marshall is sayin
Darren New wrote:
> David Hopwood wrote:
>
[...]
>> Apparently, Hermes (at least the version of it described in that paper)
>> essentially forgets that is_last has been initialized at the top of the
>> loop, and so when it does the merge, it is merging 'not necessarily
>> initialized' with 'initia
David Hopwood wrote:
> Darren New wrote:
>
>>David Hopwood wrote:
>>
>>
>>>public class LoopInitTest {
>>>public static String getString() { return "foo"; }
>>>
>>>public static void main(String[] args) {
>>>String line = getString();
>>>boolean is_last = false;
>>>
>>>
Marshall schrieb:
> No. The variable is the table, not the records.
In your examples, yes.
> Relations are not arrays.
They are, in all ways that matter for aliasing:
They are a collection of mutable data, accessible via selector values.
> Records are not lvalues.
Agreed, but they have identi
Marshall schrieb:
> Chris Smith wrote:
>> Joachim Durchholz <[EMAIL PROTECTED]> wrote:
>> I *think* I understand Marshall here. When you are saying "assignment",
>> you mean assignment to values of attributes within tuples of the cell.
>> When Marshall is saying "assignment", he seems to mean assi
Darren New wrote:
> David Hopwood wrote:
>
>> public class LoopInitTest {
>> public static String getString() { return "foo"; }
>>
>> public static void main(String[] args) {
>> String line = getString();
>> boolean is_last = false;
>>
>> while (!is_last) {
>>
Marshall <[EMAIL PROTECTED]> wrote:
> Yes, these *performance* issues make assignment prohibitive for
> real-world use, at least if we are talking about data management
> in the large. This is not the same thing as saying the resulting
> language is a toy language, though; its semantics are quite
>
Chris Smith wrote:
> Marshall <[EMAIL PROTECTED]> wrote:
> > > If the relations are to
> > > be considered opaque, then there's clearly no aliasing going on.
> >
> > Not certain I understand, but I think I agree.
>
> My condition, though, was that relations be opaque. Since you will be
> violating
Darren New wrote:
> Now, if the "insert line into inputs" actually unset "line", then yes,
> you're right, Hermes would complain about this.
Oh, I see. You translated from Hermes into Java, and Java doesn't have
the "insert into" statement. Indeed, the line you commented out is
*exactly* what's
David Hopwood wrote:
>
> public class LoopInitTest {
> public static String getString() { return "foo"; }
>
> public static void main(String[] args) {
> String line = getString();
> boolean is_last = false;
>
> while (!is_last) {
> if (line.charAt(0) =
David Hopwood wrote:
> Darren New wrote:
>
>>From what I can determine, the authors seem to imply that typestate is
>>dataflow analysis modified in (at least) two ways:
>>
>>1) When control flow joins, the new typestate is the intersection of
>>typestates coming into the join, where as dataflow an
Marshall <[EMAIL PROTECTED]> wrote:
> > If the relations are to
> > be considered opaque, then there's clearly no aliasing going on.
>
> Not certain I understand, but I think I agree.
My condition, though, was that relations be opaque. Since you will be
violating that condition further on down,
Darren New wrote:
> From what I can determine, the authors seem to imply that typestate is
> dataflow analysis modified in (at least) two ways:
>
> 1) When control flow joins, the new typestate is the intersection of
> typestates coming into the join, where as dataflow analysis doesn't
> guarantee
Chris Smith wrote:
> Marshall <[EMAIL PROTECTED]> wrote:
> > We seem to have slipped back from the hypothetical relation language
> > with only assignement back to SQL.
>
> [...]
> I don't see how such a language (limited to assignment of entire
> relations) is particularly helpful to consider.
I
Marshall wrote:
>
> I am having a hard time with this very broad definition of aliasing.
How about this definition: Consider three variables, i, j, and k, and
a functional equivalence predicate (EQUIVALENT(i, j) returns true if
for every pure function F, F(i) = F(j)). Now suppose i and j are
EQ
Marshall wrote:
> I would propose that variables have identity, and values do not.
> In part this is via the supplied definition of identity, in which, when
> you change one thing, if something else changes as well, they
> share identity.
Maybe you gave a better definition the first time, but this
Marshall <[EMAIL PROTECTED]> wrote:
> We seem to have slipped back from the hypothetical relation language
> with only assignement back to SQL.
I missed the point where we started discussing such a language. I
suspect it was while some of us were still operating under the
misconception that you
Joachim Durchholz wrote:
> of no assertion language that can express such temporal relationships,
> and even if there is (I'm pretty sure there is), I'm rather sceptical
> that programmers would be able to write correct assertions, or correctly
> interpret them - temporal logic offers several tr
Chris Smith wrote:
> Darren New <[EMAIL PROTECTED]> wrote:
>
>>I'm not sure what linear or uniqueness typing is. It's typestate, and if
>>I remember correctly the papers I read 10 years ago, the folks at
>>TJWatson that invented Hermes also invented the concept of typestate.
>>They at least cl
Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> Marshall schrieb:
> >>> Good point. Perhaps I should have said "relational algebra +
> >>> variables with assignment." It is interesting to consider
> >>> assignment vs. the more restricted update operators: insert,
> >>
Chris Smith wrote:
> Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> > I fail to see an example that would support such a claim.
> >
> > On the other hand, UPDATE can assign any value to any field of any
> > record, so it's doing exactly what an assignment does. INSERT/DELETE can
> > create resp. de
Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> I fail to see an example that would support such a claim.
>
> On the other hand, UPDATE can assign any value to any field of any
> record, so it's doing exactly what an assignment does. INSERT/DELETE can
> create resp. destroy records, which is what
Rob Warnock schrieb:
> Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> +---
> | INSERT cannot be expressed in terms of assignment. INSERT creates a new
> | record; there's no way that assignment in a language like C can create a
> | new data structure! The same goes for DELETE.
> +--
Chris Smith schrieb:
> David Hopwood <[EMAIL PROTECTED]> wrote:
>> Chris Smith wrote:
>>> If checked by execution, yes. In which case, I am trying to get my head
>>> around how it's any more true to say that functional languages are
>>> compilable postconditions than to say the same of imperativ
Joachim Durchholz <[EMAIL PROTECTED]> wrote:
+---
| INSERT cannot be expressed in terms of assignment. INSERT creates a new
| record; there's no way that assignment in a language like C can create a
| new data structure! The same goes for DELETE.
+---
Well, what about "
Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> Good point. Perhaps I should have said "relational algebra +
>>> variables with assignment." It is interesting to consider
>>> assignment vs. the more restricted update operators: insert,
>>> update, delete.
>> Actually I see it
Andreas Rossberg <[EMAIL PROTECTED]> writes:
>Uh, aliasing all over the place! Actually, I think that logic
>programming, usually based on deep unification, brings by far the worst
>incarnation of aliasing issues to the table.
I agree that deep unification, as implemented in Prolog, brings with
Darren New <[EMAIL PROTECTED]> wrote:
> I'm not sure what linear or uniqueness typing is. It's typestate, and if
> I remember correctly the papers I read 10 years ago, the folks at
> TJWatson that invented Hermes also invented the concept of typestate.
> They at least claim to have coined the te
David Hopwood <[EMAIL PROTECTED]> wrote:
> Chris Smith wrote:
> > If checked by execution, yes. In which case, I am trying to get my head
> > around how it's any more true to say that functional languages are
> > compilable postconditions than to say the same of imperative languages.
>
> A post
Joachim Durchholz wrote:
> Marshall schrieb:
> >
> > Good point. Perhaps I should have said "relational algebra +
> > variables with assignment." It is interesting to consider
> > assignment vs. the more restricted update operators: insert,
> > update, delete.
>
> Actually I see it the other way ro
Marshall schrieb:
>
> Good point. Perhaps I should have said "relational algebra +
> variables with assignment." It is interesting to consider
> assignment vs. the more restricted update operators: insert,
> update, delete.
Actually I see it the other way round: assignment is strictly less
power
Marshall <[EMAIL PROTECTED]> wrote:
> Is it possible you're being distracted by the syntax? WHERE is a
> binary operation taking a relation and a filter function. I don't
> think of filters as being like array indexing; do they appear
> analogous to you? (Always a difficult question because often
>
We Chris's stick together, as always.
Marshall <[EMAIL PROTECTED]> wrote:
> > Unfortunately, they are the right level. Actually,the right level
> > might even be lower, the fields within a record, but that's moving
> > even farther away from the direction you wish to go. The right level
> > is t
Chris F Clark wrote:
> "Marshall" <[EMAIL PROTECTED]> wrote:
> > In general, I feel that "records" are not the right conceptual
> > level to think about.
>
> Unfortunately, they are the right level. Actually,the right level
> might even be lower, the fields within a record, but that's moving
> eve
Joachim Durchholz wrote:
> Marshall schrieb:
>
> > But what you descrbe is certainly *not* possible in the
> > relational algebra; alas that SQL doesn't hew closer
> > to it. Would you agree?
>
> Yup, SQL (particularly its update semantics) aren't relational semantics.
> Still, it's SQL we've been
Chris F Clark schreef:
> If you have a fixed database, and you do two selects which specify the
> same sets of fields to be selected and the same keys to select records
> with, one expects the two selects to return the same values.
When your "fixed" means read-only, or (fully) locked, then yes.
"Marshall" <[EMAIL PROTECTED]> wrote:
> In general, I feel that "records" are not the right conceptual
> level to think about.
Unfortunately, they are the right level. Actually,the right level
might even be lower, the fields within a record, but that's moving
even farther away from the direction
Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> I would say, records in SQL have value, and their
>>> identity is exactly their value.
>>
>> Definitely not. You can have two equal records and update just one of
>> them, yielding non-equal records; by my definition (and by int
Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> As I said elsewhere, the record has an identity even though it isn't
> >> explicit in SQL.
> >
> > H. What can this mean?
> >
> > In general, I feel that "records" are not the right conceptual
> > level to think abou
Marshall schrieb:
> Joachim Durchholz wrote:
>> As I said elsewhere, the record has an identity even though it isn't
>> explicit in SQL.
>
> H. What can this mean?
>
> In general, I feel that "records" are not the right conceptual
> level to think about.
They are, when it comes to aliasing o
Joachim Durchholz wrote:
> Marshall schrieb:
>
> >> In some cases, you need an additional level of conceptual indirection -
> >> instead of *doing* the updates, you write a function that *describes* them.
> >
> > But then what do you do with that function?
>
> I pass it to an engine that's imperati
Joachim Durchholz wrote:
>
> You can have aliasing without pointers; e.g. arrays are fully sufficient.
> If i = j, then a [i] and a [j] are aliases of the same object.
"Marshall" <[EMAIL PROTECTED]> writes:
> I am having a hard time with this very broad definition of aliasing.
> Would we also
Marshall wrote...
> I am having a hard time with this very broad definition of aliasing.
> Would we also say that a[1+1] and a[2] are aliases? It seems
> to me, above, that we have only a, and with only one variable
> there can be no aliasing.
The problem with this (and with the relational one as
Marshall schrieb:
> Joachim Durchholz wrote:
>> You can have aliasing without pointers; e.g. arrays are fully sufficient.
>> If i = j, then a [i] and a [j] are aliases of the same object.
>
> I am having a hard time with this very broad definition of aliasing.
> Would we also say that a[1+1] and a
Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> What about my example of SQL? Mutation, no pointers, no aliasing.
>>> Yet: useful.
>> Sorry, but SQL does have aliasing.
>
> Well. I suppose we do not have an agreed upon definition
> of aliasing, so it is hard to evaluate eithe
Marshall wrote:
> Joe Marshall wrote:
> > Marshall wrote:
> > >
> > > Consider the following Java fragment:
> > >
> > > void foo() {
> > > int i = 0;
> > > int j = 0;
> > >
> > > // put any code here you want
> > >
> > > j = 1;
> > > i = 2;
> > > // check value of j here. It is still 1
Andreas Rossberg wrote:
> OK, this is interesting. I don't know Hermes, is this sort of like a
> dynamically checked equivalent of linear or uniqueness typing?
I'm not sure what linear or uniqueness typing is. It's typestate, and if
I remember correctly the papers I read 10 years ago, the folks
Marshall wrote:
> Andreas Rossberg wrote:
> >
> > And note that even with second-class state you can still have aliasing
> > issues - you just need mutable arrays and pass around indices. Keys in
> > databases are a more general form of the same problem.
>
> So for array a, you would claim that "a[
Joachim Durchholz wrote:
>
> You can have aliasing without pointers; e.g. arrays are fully sufficient.
> If i = j, then a [i] and a [j] are aliases of the same object.
I am having a hard time with this very broad definition of aliasing.
Would we also say that a[1+1] and a[2] are aliases? It seems
Joachim Durchholz wrote:
> Marshall schrieb:
> > void foo() {
> > int i = 0;
> > int j = 0;
> > j = 1;
> > i = 2;
> > // check value of j here. It is still 1, no matter what you filled
> > // in above.
> > // The assignment to i cannot be made to affect the value of j.
> > }
> >
> >
Andreas Rossberg wrote:
> Marshall wrote:
> >
> > After all, what are the alternatives? Purely-functional
> > languages remove themselves from a large class of
> > problems that I consider important: data management.
>
> Maybe, but I have yet to see how second-class variables are really more
> adeq
Joachim Durchholz wrote:
> Marshall schrieb:
> > What about my example of SQL? Mutation, no pointers, no aliasing.
> > Yet: useful.
>
> Sorry, but SQL does have aliasing.
Well. I suppose we do not have an agreed upon definition
of aliasing, so it is hard to evaluate either way. I would
propose usi
Marshall schrieb:
> Joachim Durchholz wrote:
>> It's just that I know that it's viable to give up destructive updates.
>> Giving up pointers is a far more massive restriction.
>
> Oddly, I feel the opposite. While it's true there are many domains
> for which purely functional programming is a fine
Marshall schrieb:
> By your definition, "pointer" and "variable" are synonyms. That doesn't
> seem like a good idea to me. (What if i and j end up in registers?
> I have not heard it said that registers have addresses.)
There are no registers in the JVM ;-P
More specifically, where Joe said "poin
Marshall schrieb:
> void foo() {
> int i = 0;
> int j = 0;
> j = 1;
> i = 2;
> // check value of j here. It is still 1, no matter what you filled
> // in above.
> // The assignment to i cannot be made to affect the value of j.
> }
>
> Those two local primitive variables cannot be ma
Marshall wrote:
>
> After all, what are the alternatives? Purely-functional
> languages remove themselves from a large class of
> problems that I consider important: data management.
Maybe, but I have yet to see how second-class variables are really more
adequate in dealing with it.
And note th
Darren New wrote:
> Andreas Rossberg wrote:
>
>> Yes, technically you are right. But this makes a pretty weak notion of
>> mutability. All stateful data structures had to stay within their
>> lexical scope, and could never be passed to a function.
>
> Not really. The way Hermes handles this is
Marshall schrieb:
> What about my example of SQL? Mutation, no pointers, no aliasing.
> Yet: useful.
Sorry, but SQL does have aliasing.
E.g. if you have records that have name="John", surname="Doe", the
statements
SELECT * FROM persons WHERE name = "John"
and
SELECT * FROM persons WHERE na
Chris Smith wrote:
> Marshall <[EMAIL PROTECTED]> wrote:
> > > What you are asking for is some subset of identity, and I've not yet
> > > succeeded in understanding exactly what it is or what its limits are...
> > > except that so far, it seems to have everything to do with pointers or
> > > aliasi
George Neuner wrote:
> On 13 Jul 2006 08:45:49 -0700, "Marshall" <[EMAIL PROTECTED]>
> wrote:
> >
> >On the other hand, there is no problem domain for which pointers
> >are a requirement. I agree they are deucedly convenient, though.
> >
>
> I would argue that pointers/references _are_ a requiremen
On 13 Jul 2006 08:45:49 -0700, "Marshall" <[EMAIL PROTECTED]>
wrote:
>
>On the other hand, there is no problem domain for which pointers
>are a requirement. I agree they are deucedly convenient, though.
>
I would argue that pointers/references _are_ a requirement for I/O. I
know of no workable me
Marshall <[EMAIL PROTECTED]> wrote:
> > What you are asking for is some subset of identity, and I've not yet
> > succeeded in understanding exactly what it is or what its limits are...
> > except that so far, it seems to have everything to do with pointers or
> > aliasing.
>
> Perhaps it is specif
Chris Smith wrote:
> Marshall <[EMAIL PROTECTED]> wrote:
> > Chris Smith wrote:
> > > Darren New <[EMAIL PROTECTED]> wrote:
> > > > Chris Smith wrote:
> > > > > Unless I'm missing your point, I disagree with your disagreement.
> > > > > Mutability only makes sense because of object identity (in the
Chris Smith wrote:
> David Hopwood <[EMAIL PROTECTED]> wrote:
>
>>This is true, but note that postconditions also need to be efficient
>>if we are going to execute them.
>
> If checked by execution, yes. In which case, I am trying to get my head
> around how it's any more true to say that funct
Marshall <[EMAIL PROTECTED]> wrote:
> Chris Smith wrote:
> > Darren New <[EMAIL PROTECTED]> wrote:
> > > Chris Smith wrote:
> > > > Unless I'm missing your point, I disagree with your disagreement.
> > > > Mutability only makes sense because of object identity (in the generic
> > > > sense; no OO g
Chris Smith wrote:
> Darren New <[EMAIL PROTECTED]> wrote:
> > Chris Smith wrote:
> > > Unless I'm missing your point, I disagree with your disagreement.
> > > Mutability only makes sense because of object identity (in the generic
> > > sense; no OO going on here).
> >
> > Depends what you mean by
Joe Marshall wrote:
> Marshall wrote:
> >
> > Consider the following Java fragment:
> >
> > void foo() {
> > int i = 0;
> > int j = 0;
> >
> > // put any code here you want
> >
> > j = 1;
> > i = 2;
> > // check value of j here. It is still 1, no matter what you filled in
> > above.
> >
Marshall <[EMAIL PROTECTED]> wrote:
+---
| Joachim Durchholz wrote:
| > Actually SQL has references - they are called "primary keys", but they
| > are references nevertheless.
|
| I strongly object; this is quite incorrect. I grant you that from the
| 50,000 foot level they appear iden
David Hopwood <[EMAIL PROTECTED]> wrote:
> This is true, but note that postconditions also need to be efficient
> if we are going to execute them.
If checked by execution, yes. In which case, I am trying to get my head
around how it's any more true to say that functional languages are
compilabl
Darren New <[EMAIL PROTECTED]> wrote:
> Chris Smith wrote:
> > Unless I'm missing your point, I disagree with your disagreement.
> > Mutability only makes sense because of object identity (in the generic
> > sense; no OO going on here).
>
> Depends what you mean by "object".
>
> int x = 6; in
Marshall wrote:
>
> Consider the following Java fragment:
>
> void foo() {
> int i = 0;
> int j = 0;
>
> // put any code here you want
>
> j = 1;
> i = 2;
> // check value of j here. It is still 1, no matter what you filled in
> above.
> // The assignment to i cannot be made to affec
Joe Marshall wrote:
> Marshall wrote:
> >
> > Again, I disagree: it is posible to have mutability without
> > pointers/identity/objects.
>
> I think you are wrong, but before I make a complete ass out of myself,
> I have to ask what you mean by `mutability'. (And
> pointers/identity/objects, for t
Chris Smith wrote:
> Joachim Durchholz <[EMAIL PROTECTED]> wrote:
>
>>OTOH, isn't that the grail that many people have been searching for:
>>programming by simply declaring the results that they want to see?
>
> Possibly.
>
>>No, FPLs are actually just that: compilable postconditions.
>
> This
Joachim Durchholz wrote:
> Marshall schrieb:
> > Mutability by itself does not imply identity.
>
> Well, the implication certainly holds from identity to mutability.
> The only definition of identity that I found to hold up for all kinds of
> references (pointers, shared-memory identifiers, URLs et
Marshall wrote:
> David Hopwood wrote:
>>Marshall wrote:
>>
>>>Wouldn't it be possible to do them at compile time? (Although
>>>this raises decidability issues.)
>>
>>It is certainly possible to prove statically that some assertions cannot fail.
>>
>>The ESC/Java 2 (http://secure.ucd.ie/products/op
Marshall wrote:
>
> Again, I disagree: it is posible to have mutability without
> pointers/identity/objects.
I think you are wrong, but before I make a complete ass out of myself,
I have to ask what you mean by `mutability'. (And
pointers/identity/objects, for that matter.)
Alan Bawden discusse
Chris Smith wrote:
> Unless I'm missing your point, I disagree with your disagreement.
> Mutability only makes sense because of object identity (in the generic
> sense; no OO going on here).
Depends what you mean by "object".
int x = 6; int y = 5; x = y;
I'd say x was mutable, with no "ident
Marshall <[EMAIL PROTECTED]> wrote:
> Hmmm, well, I cannot agree. You've defined away the pointers
> but then slipped them back in again by assumption ("objects
> of these types have identity".)
>
> First let me say that the terminology is somewhat problematic.
> For the specific issue being discu
Marshall schrieb:
> Mutability by itself does not imply identity.
Well, the implication certainly holds from identity to mutability.
The only definition of identity that I found to hold up for all kinds of
references (pointers, shared-memory identifiers, URLs etc.) is this:
Two pieces of data ar
Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> OTOH, isn't that the grail that many people have been searching for:
> programming by simply declaring the results that they want to see?
Possibly.
> No, FPLs are actually just that: compilable postconditions.
This seems to me a bit misleading. Pe
Andreas Rossberg wrote:
> Yes, technically you are right. But this makes a pretty weak notion of
> mutability. All stateful data structures had to stay within their
> lexical scope, and could never be passed to a function.
Not really. The way Hermes handles this is with destructive assignment.
Joachim Durchholz wrote:
> A concrete example: the
> first thing that Windows does when accepting userland data structures
> is... to copy them; this were unnecessary if the structures were immutable.
It is necessary also because the userland structures are in a different
privilege domain, and the
Marshall wrote:
>
> However if the mutable types are not first class, then there
> is no way to have the aliasing. Thus, if we do not have pointers
> or objects or identity but retain mutability, there is no aliasing
> problem.
Yes, technically you are right. But this makes a pretty weak notion o
Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> Marshall schrieb:
> >>> Joachim Durchholz wrote:
> Marshall schrieb:
> > I can see the lack of a formal model being an issue, but is the
> > imperative bit really all that much of an obstacle? How hard
> >>>
Andreas Rossberg wrote:
> Marshall wrote:
> >
> > Okay, sure. But for the problem you describe, both imperativeness
> > and the presence of pointers is each necessary but not sufficient;
> > it is the two together that causes the problem. So it strikes
> > me (again, a very minor point) as inaccura
Marshall schrieb:
> David Hopwood wrote:
>> This property is, after all, not something that the program should depend on.
>> It is determined by how good the static checker currently is, and we want to
>> be
>> able to improve checkers (and perhaps even allow them to regress slightly in
>> order t
Darren New schrieb:
> Joachim Durchholz wrote:
>> Actually, in a functional programming language (FPL), you write just
>> the postconditions and let the compiler generate the code for you.
>
> Certainly. And my point is that the postcondition describing "all valid
> chess boards reachable from t
Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> Joachim Durchholz wrote:
Marshall schrieb:
> I can see the lack of a formal model being an issue, but is the
> imperative bit really all that much of an obstacle? How hard
> is it really to deal with assignment?
Marshall wrote:
>
> Okay, sure. But for the problem you describe, both imperativeness
> and the presence of pointers is each necessary but not sufficient;
> it is the two together that causes the problem. So it strikes
> me (again, a very minor point) as inaccurate to describe this as
> a problem
Marshall <[EMAIL PROTECTED]> wrote:
> David Hopwood wrote:
> > Marshall wrote:
> > > Mightn't it also be possible to
> > > leave it up to the programmer whether a given contract
> > > was compile-time or runtime?
> >
> > That would be possible, but IMHO a better option would be for an IDE to give
David Hopwood wrote:
> Marshall wrote:
>
> > Wouldn't it be possible to do them at compile time? (Although
> > this raises decidability issues.)
>
> It is certainly possible to prove statically that some assertions cannot fail.
>
> The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/d
Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> Marshall schrieb:
> >>> I can see the lack of a formal model being an issue, but is the
> >>> imperative bit really all that much of an obstacle? How hard
> >>> is it really to deal with assignment? Or does the issue hav
Marshall wrote:
> Joachim Durchholz wrote:
[...]
>>Preconditions/postconditions can express anything you want, and they are
>>an absolutely natural extensions of what's commonly called a type
>>(actually the more powerful type systems have quite a broad overlap with
>>assertions).
>>I'd essentially
Joachim Durchholz wrote:
> Actually, in a functional programming language (FPL), you write just the
> postconditions and let the compiler generate the code for you.
Certainly. And my point is that the postcondition describing "all valid
chess boards reachable from this one" is pretty much going
Darren New schrieb:
> There are also problems with the complexity of things. Imagine a
> chess-playing game trying to describe the "generate moves" routine.
> Precondition: An input board with a valid configuration of chess pieces.
> Postcondition: An array of boards with possible next moves for
Marshall schrieb:
> Joachim Durchholz wrote:
>> Marshall schrieb:
>>> I can see the lack of a formal model being an issue, but is the
>>> imperative bit really all that much of an obstacle? How hard
>>> is it really to deal with assignment? Or does the issue have
>>> more to do with pointers, alias
Joachim Durchholz wrote:
> Marshall schrieb:
> > I can see the lack of a formal model being an issue, but is the
> > imperative bit really all that much of an obstacle? How hard
> > is it really to deal with assignment? Or does the issue have
> > more to do with pointers, aliasing, etc.?
>
> Actual
Marshall schrieb:
> So, what exactly separates a precondition from a postcondition
> from an invariant? I have always imagined that one writes
> assertions on parameters and return values, and those
> assertions that only reference parameters were preconditions
> and those which also referenced ret
Marshall schrieb:
> I can see the lack of a formal model being an issue, but is the
> imperative bit really all that much of an obstacle? How hard
> is it really to deal with assignment? Or does the issue have
> more to do with pointers, aliasing, etc.?
Actually aliasing is *the* hard issue.
Just
1 - 100 of 175 matches
Mail list logo
