is python Object oriented??

[Mark Wooding]

Steven D'Aprano <steven at REMOVE.THIS.cybersource.com.au> writes:

> Now, that's a toy example. Languages like Ada make correctness proofs, 
> well, perhaps not easy, but merely difficult compared to impossible for 
> languages like Python.

Say `generally impractical' rather than `impossible' and I'll agree with
you.  But I'm not actually sure that the situation for Python with
respect to correctness proofs is significantly harder than it is for C.
Certainly Ada (or at least dialects of Ada) have features which make
proof-supporting tools easier; I'm not aware of such proof support for
other languages.

Actually, if you're starting from a formal specification in Z, say, and
implementing in Python, well, the Z checker will already have ensured
that your specification is well typed; your proof that the
implementation follows the specification will automatically contain a
well-typed-ness proof of your implementation regardless of whether the
compiler provides static verification.

> To bring it back to private/public attributes, side-effects make 
> correctness proofs difficult. Modifications of attributes are side-
> effects. When attributes are subject to being modified by arbitrary code, 
> it is harder to reason about the correctness of the code:
>
> class Inverter(object):
>     def __init__(self, x):
>         # Pre-condition: x is always a float
>         if x:
>             self.x = x
>         else:
>             raise ValueError("x must not be zero")
>         # Post-condition: if self.x exists, it is a non-zero float
>     def invert(self):
>         return 1.0/self.x
>
>
> Is method invert correct?

I'd argue that it isn't, and in fact that the specification is wrong.
In particular, it ought to be a precondition that x is nonzero.  At this
point you can dump the explicit check at the cost of imposing a proof
obligation on the caller.

> No, it is not, because the invariant that self.x is non-zero may have 
> been broken by some arbitrary piece of code elsewhere. 

It's not stated as an invariant.  It's stated as a post-condition, which
is indeed true (almost[1]) regardless of the behaviour of other parts of
the program.

[1] A subclass may have already set self.x before invoking
    Inverter.__init__.  If you explicitly `del self.x' before raising
    the exception, the subclass can still defeat you by passing the
    reference to the half-constructed object to another thread which
    mutates the object at an inconvenient time.  I mention all of this
    merely to avoid pedantry in follow-ups.

I'd also argue that maintaining the invariant about self.x is the
responsibility of code that messes with self.x, and therefore it is
/legitimate/ to modify self.x from external code which maintains the
invariant.

> Our ability to reason about the correctness of the code is weakened
> significantly.  Sticking an underscore in front of x does not help:
> there's nothing to stop some arbitrary function elsewhere changing _x
> to zero.

Dichotomy for you.

  * EITHER the other code is written to the same high standards, in
    which case it will come with appropriate specifications,
    preconditions, postconditions, invariants and proofs for whatever it
    does, even -- especially -- if it involves grubbily messing about
    with your module's innards (so everything is fine);

  * OR the other code doesn't meet your high standards, in which case
    all bets are off anyway, from the point of view of formal-methods
    types at any rate (so you can wash your hands of the whole affair).

> (1) Paranoia. Make the developer responsible for checking everything all 
> the time:
[...]
> (2) Hope the error never occurs, and if it does, let the caller deal with 
> it.
[...]
> There is a third strategy, sadly not available to Python programmers: 
> prevention by catching potential errors at compile-time.

Four: Describe your interface clearly, specify the behaviour of
functions and so on; and leave whoever messes with your module with the
task of proving -- to whatever level of formality is required by their
project -- that what they've done is sane and reasonable.

In fact, since whatever one does in a project should be held to this
standard, whether it involves grubbing about inside undocumented
internals or not, there's nothing particularly special about this case.
Good job, really, since Python doesn't distinguish either. ;-)

-- [mdw]