Design by contract for python

[adsharma]

I was not aware of Nagini or Viper work when I wrote this:

https://adsharma.github.io/pysmt/

I worked on https://github.com/adsharma/py2many/ - a transpiler in the past and am looking into adding some static verification capabilities before generating code in other languages such as C++ and Rust.

A few questions:

• Can the Nagini/Viper/Boogie/Z3 stack be collapsed to: a subset of python -> z3?
• I'm looking to build a boogie like thing with pythonic syntax (linked in the blog post above). I read something about B-SMT in a ETH paper. Agree that infix syntax is more human readable.
• Can we maintain compatibility of input source with python3? In my proposal, if smt.pre would evaluate to False and python interpreter ignores that block. I like requires/ensures better than pre/post.
• Datatypes: I've built something using @sealed for py2many. Perhaps we can reuse it.
• Can we use python as the intermediate language instead of viper?

Let me know if any of this sounds interesting.

[marcoeilers]

I think this is a bit difficult to discuss in Github comments (I'm not sure I completely understand all of your questions, and some of my answers would be rather long as well); if you'd be interested, we could have a quick chat about this on Skype/Zoom/... instead?

[adsharma]

py2many/py2many#443 is a demo of translating a python ADT that uses the @Sealed syntax to z3 -smt2 compatible format.

Also edited the text above for legibility.

The flow I'm thinking about is:

1. static python
2. contract python - no spec yet, but this will be a different subset of python
3. smt2 sexpression accepted by z3 -smt2

(1) -> py2many -verify -> (2) -> py2many --smt=1 -> (3) (proceed to next step only after verification)
(1) -> py2many -> C++/Rust/Go -> Verified executable

I'll email you to coordinate an in person chat.