Dafny vs z3

[adsharma]

Great idea to try and verify python code before generating an executable!

I work on https://github.com/adsharma/py2many. Recently I added the capability to transpile python -> smt2 (the sexpression based language that z3 uses). py2many/py2many@a89e5ad

Couple of questions for you:

• Why dafny and why not z3 (the underlying engine used by dafny)
• Using comment based pre/post condition vs getting them parsed via python AST (https://adsharma.github.io/pysmt/)
• Have you looked into https://github.com/caterinaurban/Typpete, which is already using z3?

I'm running into some problems expressing simple type constraints in z3. Asking around for help. Would love to collaborate.

[adsharma]

My fork of Typpete here:

https://github.com/adsharma/Typpete

Still trying to make progress on fixed width types and other constraints.

[arsalan0c]

Great idea to try and verify python code before generating an executable!

I work on https://github.com/adsharma/py2many. Recently I added the capability to transpile python -> smt2 (the sexpression based language that z3 uses). adsharma/py2many@a89e5ad

Couple of questions for you:

• Why dafny and why not z3 (the underlying engine used by dafny)
• Using comment based pre/post condition vs getting them parsed via python AST (https://adsharma.github.io/pysmt/)
• Have you looked into https://github.com/caterinaurban/Typpete, which is already using z3?

I'm running into some problems expressing simple type constraints in z3. Asking around for help. Would love to collaborate.

Hi, sorry for the delayed response. Thank you for sharing py2many, really interesting project!

I was not aware of Python having a contract syntax (PEP316), this would have made use of the Python parser more compelling.

Dafny was used over Z3 due to the project time constraints. I was familiar with the former and but not the latter. I would be keen on learning Z3 in the future. I have not looked into Typpete but its type inference would be really useful for eg. supporting list concatenation with +.

[adsharma]

Typpete seems inactive. I've forked it here with the intention of uploading to pypi eventually

https://github.com/adsharma/Typpete

Try a test case such as:

def foo():
    return [42]

def add(a, b):
    return a+b

c = foo()
d = add([], c)

PEP 316 is from 2003 with a status "deferred". I'm proposing a new syntax in the blog post above.

Leaning towards if smt.required/ensures. When executing on top of the normal python interpreter, these would eval to false and hence skipped.

In the verified python mode, they actually have an effect.

I spent some time studying Dafny here dafny-lang/dafny#1323
Boogie seems interesting. Looking to build a pythonic syntax for Boogie such as:

https://github.com/adsharma/py2many/blob/main/tests/cases/demorgan.py

This code can't be executed. It's a way of declaring constraints, which is translated to the underlying prover (z3).

Also see: py2many/py2many#440