On Jan 16, 2006, at 6:42 PM, Chris Richardson wrote:
Greg;
Suppose we talk about doing a pratical model as a means of
applying your
hypothetical model. It is much easier to understand a process if
you can
tie it to a real life situation. But first, instead of trying to
hit all of
your shopping list in one go, let's just start with the most simple to
implement. Once we understand how this is working, then we add
additional
functionality and complexity. In this way, we understand the
impact of each
additional feature we add on the model. This is how one eats the
elephant,
one bite at a time (and pray for enough space in the refrigerator
for the
leftovers).
Best wishes; Chris
Well, here's a really simple example. The method of invariants (pre-
and post-conditions) can be used to prove correctness of simple
programs when concurrency is not an issue. In fact, I've written
formal proofs that certain programs behave as required. But when a
program no longer runs in isolation, it's possible future depends on
the (possibly unknown) behavior of other programs, or even timing
issues. The possibility of interference of this type makes it very
difficult to find general ways of even defining, much less proving
compositionality. Within the context of a single process (no I/O) you
can, in principe, prove correctness of program components (e.g.,
subroutines) and then prove that they are being combined correctly.
But in the presence of concurrency, a program ceases to be the sum of
its parts, or, if you will, the effect of a "part" depends on the
context in which it is used.
===
Gregory Woodhouse
[EMAIL PROTECTED]
"You must unlearn what you have learned."
--Yoda
-------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc. Do you grep through log files
for problems? Stop! Download the new AJAX search engine that makes
searching your log files as easy as surfing the web. DOWNLOAD SPLUNK!
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=103432&bid=230486&dat=121642
_______________________________________________
Hardhats-members mailing list
Hardhats-members@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hardhats-members