[Python-Dev] Static checker for common Python programming errors

[Guido van Rossum]

Please also check python-static-type-checking at googlegroups.com.
On Nov 18, 2014 3:06 AM, "Stefan Bucur" <stefan.bucur at gmail.com> wrote:

> Thanks for the pointer! There seem indeed to be more formal analysis tools
> for JavaScript than for Python (e.g., the most recent one for JS I know of
> is the Jalangi framework [1]). I assume the main reason is that JavaScript
> is standardized and somewhat simpler, so it's easier to construct formal
> specs for all language features than it is for Python, which is also
> evolving faster and relies on a lot of hard-to-model native functionality.
>
> That's why I'm planning to reuse as much as possible the "implicit specs"
> of the interpreter implementation, instead of re-stating them in an
> explicit model.
>
> We already have an execution engine that uses the interpreter to
> automatically explore multiple paths through a piece of Python code (you
> can read here [2] the academic paper, with case studies for Python and
> Lua). In turn, we could use that engine to discover paths, while checking
> program properties along each path.
>
> Guido's suggestion for a type checker raises some interesting applications
> of this multi-path analysis. For instance, we could examine the type of the
> objects assigned to a static variable across all discovered execution paths
> and determine its consistency. This analysis could either start with no
> type annotations and output suggested types, or take existing annotations
> and check them against the actual types.
>
> Thanks again,
> Stefan
>
> [1] https://github.com/SRA-SiliconValley/jalangi
> [2] http://dslab.epfl.ch/pubs/chef.pdf
>
> On Mon Nov 17 2014 at 8:50:21 PM Francis Giraldeau <
> francis.giraldeau at gmail.com> wrote:
>
>> If I may, there are prior work on JavaScript that may be worth
>> investigating. Formal verification of dynamically typed software is a
>> challenging endeavour, but it is very valuable to avoid errors at runtime,
>> providing benefits from strongly type language without the rigidity.
>>
>> http://cs.au.dk/~amoeller/papers/tajs/
>>
>> Good luck!
>>
>> Francis
>>
>> 2014-11-17 9:49 GMT-05:00 Stefan Bucur <stefan.bucur at gmail.com>:
>>
>>> I'm developing a Python static analysis tool that flags common
>>> programming errors in Python programs. The tool is meant to complement
>>> other tools like Pylint (which perform checks at lexical and syntactic
>>> level) by going deeper with the code analysis and keeping track of the
>>> possible control flow paths in the program (path-sensitive analysis).
>>>
>>> For instance, a path-sensitive analysis detects that the following
>>> snippet of code would raise an AttributeError exception:
>>>
>>> if object is None: # If the True branch is taken, we know the object is
>>> None
>>>   object.doSomething() # ... so this statement would always fail
>>>
>>> I'm writing first to the Python developers themselves to ask, in their
>>> experience, what common pitfalls in the language & its standard library
>>> such a static checker should look for. For instance, here [1] is a list of
>>> static checks for the C++ language, as part of the Clang static analyzer
>>> project.
>>>
>>> My preliminary list of Python checks is quite rudimentary, but maybe
>>> could serve as a discussion starter:
>>>
>>> * Proper Unicode handling (for 2.x)
>>>   - encode() is not called on str object
>>>   - decode() is not called on unicode object
>>> * Check for integer division by zero
>>> * Check for None object dereferences
>>>
>>> Thanks a lot,
>>> Stefan Bucur
>>>
>>> [1] http://clang-analyzer.llvm.org/available_checks.html
>>>
>>>
>>> _______________________________________________
>>> Python-Dev mailing list
>>> Python-Dev at python.org
>>> https://mail.python.org/mailman/listinfo/python-dev
>>>
>> Unsubscribe:
>>> https://mail.python.org/mailman/options/python-dev/francis.giraldeau%40gmail.com
>>>
>>>
>>
> _______________________________________________
> Python-Dev mailing list
> Python-Dev at python.org
> https://mail.python.org/mailman/listinfo/python-dev
> Unsubscribe:
> https://mail.python.org/mailman/options/python-dev/guido%40python.org
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-dev/attachments/20141118/96ab0719/attachment.html>