Please also check python-static-type-check...@googlegroups.com. On Nov 18, 2014 3:06 AM, "Stefan Bucur" <stefan.bu...@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.girald...@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.bu...@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@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@python.org > https://mail.python.org/mailman/listinfo/python-dev > Unsubscribe: > https://mail.python.org/mailman/options/python-dev/guido%40python.org > >
_______________________________________________ Python-Dev mailing list Python-Dev@python.org https://mail.python.org/mailman/listinfo/python-dev Unsubscribe: https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com