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 return values were postconditions.
> Wouldn't that be easy enough to determine automatically?
Sure.
Actually this can be done in an even simpler fashion; e.g. in Eiffel, it
is (forgive me if I got the details wrong, it's been several years since
I last coded in it):
foo (params): result_type is
require
-- list of assertions; these become preconditions
do
-- subroutine body
ensure
-- list of assertions; these become postconditions
end
> And what's an invariant anyway?
In general, it's a postcondition to all routines that create or modify a
data structure of a given type.
Eiffel does an additional check at routine entry, but that's just a
last-ditch line of defense against invariant destruction via aliases,
not a conceptual thing. Keep aliases under control via modes (i.e.
"unaliasable" marks on local data to prevent aliases from leaving the
scope of the data structure), or via locking, or simply by disallowing
destructive updates, and you don't need the checks at routine entry anymore.
Regards,
Jo
--
http://mail.python.org/mailman/listinfo/python-list
