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 imperative languages. >> >> A postcondition must, by definition [*], be a (pure) assertion about the >> values that relevant variables will take after the execution of a subprogram. > > Okay, my objection was misplaced, then, as I misunderstood the original > statement. I had understood it to mean that programs written in pure > functional languages carry no additional information except for their > postconditions.
Oh, but that's indeed correct for pure functional languages. (Well, they *might* carry additional information anyway, but it's not a requirement to make it a programming language.) The answer that I have for your original objection may be partial, but here goes anyway: Postconditions cannot easily capture all side effects. E.g. assume there's a file-open routine but no way to test whether a given file handle was ever opened (callers are supposed to test the return code from the open() call). In an imperative language, that's a perfectly valid (though possibly not very good) library design. Now the postcondition would have to say something like "from now on, read() and write() are valid on the filehandle that I returned". I know 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 traps for the unwary. (The informal postcondition above certainly isn't complete, since it doesn't cover close(); I shunned the effort to get a wording that would correctly cover sequences like open()-close()-open(), or open()-close()-close()-open().) Regards, Jo -- http://mail.python.org/mailman/listinfo/python-list
