What is a type error?

[Darren New]

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.