PEP 3107 and stronger typing (note: probably a newbie question)
Diez B. Roggisch
deets at nospam.web.de
Fri Jul 13 11:44:05 CEST 2007
John Nagle schrieb:
> Chris Mellon wrote:
>> You can't prove a program to be correct, in the sense that it's proven
>> to do what it's supposed to do and only what it's supposed to do.
> Actually, you can prove quite a bit about programs with the right
> For example, proving that a program cannot subscript out of range is
> quite feasible. (Although not for C, where it's most needed; that language
> is just too ill-defined.)
You can - when there is input involved?
> You can prove that certain assertions about
> an object always hold when control is outside the object. You can
> prove that certain entry conditions for a function are satisfied by
> all its callers.
> Take a look at what the "Spec#" group at Microsoft is doing.
> There's also some interesting USAF work on avionics at
For example, SPARK does not support dynamic allocation of memory so
things such as pointers and heap variables are not supported.
Pardon me, but if that's the restrictions one has to impose to his
programs to make them verifiable, I'm not convinced that this is a way
to go for python - or any other language - that needs programs beyond
the most trivial tasks.
Which is not to say that trivial code couldn't have errors, and if it's
extremely cruical code, it's important that it hasn't errors. But all I
can see is that you can create trustable, simple sub-systems in such a
language. And by building upon them, you can ensure that at least these
But to stick with the example: if the path-planning of the UAV that
involves tracking a not before-known number of enemy aircrafts steers
the UAV into the ground, no proven-not-to-fail radius calculation will
More information about the Python-list