Marshall wrote:
> So, what exactly separates a precondition from a postcondition
> from an invariant?
A precondition applies to a routine/method/function and states the
conditions under which a function might be called. For example, a
precondition on "stack.pop" might be "not stack.empty", and
"socket.read" might have a precondition of "socket.is_open", and
"socket.open_a_new_connection" might have a precondition of
"socket.is_closed".
A postcondition applies to a routine/method/function and states (at
least part of) what that routine guarantees to be true when it returns,
assuming it is called with true preconditions. So "not stack.empty"
would be a postcondition of "stack.push". If your postconditions are
complete, they tell you what the routine does.
An invariant is something that applies to an entire object instance, any
time after the constructor has completed and no routine within that
instance is running (i.e., you're not in the middle of a call). There
should probably be something in there about destructors, too. So an
invariant might be "stack.is_empty == (stack.size == 0)" or perhaps
"socket.is_open implies (socket.buffer != null)" or some such.
The first problem with many of these sorts of things are that in
practice, there are lots of postconditions that are difficult to express
in any machine-readable way. The postcondition of "socket.read" is that
the buffer passed as the first argument has valid data in the first "n"
bytes, where "n" is the return value from "socket.read", unless
"socket.read" returned -1. What does "valid" mean there? It has to
match the bytes sent by some other process, possibly on another machine,
disregarding the bytes already read.
You can see how this can be hard to formalize in any particularly useful
way, unless you wind up modelling the whole universe, which is what most
of the really formalized network description techniques do.
Plus, of course, without having preconditions and postconditions for OS
calls, it's difficult to do much formally with that sort of thing.
You can imagine all sorts of I/O that would be difficult to describe,
even for things that are all in memory: what would be the postcondition
for "screen.draw_polygon"? Any set of postconditions on that routine
that don't mention that a polygon is now visible on the screen would be
difficult to take seriously.
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 the
selected team. Heck, if you could write those as assertions, you
wouldn't need the code.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
