arsalan0c/dafny-of-python

A tool for deductive verification of Python programs based on Dafny

dafny-of-python's Issues

Dafny vs z3

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.

Grammar railroad diagram

I've done a experimental tool to convert bison grammars to a kind of EBNF understood by https://www.bottlecaps.de/rr/ui to generate railroad diagrams see bellow the converted src/libs/parse/parser.ml and with some hand made changes to allow view it at https://www.bottlecaps.de/rr/ui the order of the rules could be changed to a better view of the railroad diagrams. Copy and paste the EBNF bellow on https://www.bottlecaps.de/rr/ui tab Edit Grammar then switch to the tab View Diagram.

/*
From https://github.com/arsalanc-v2/dafny-of-python/blob/master/src/libs/parse/parser.ml
*/

program ::=  stmts_plus EOF
stmts_plus ::=  /* empty */ | stmt | stmt NEWLINE stmts_plus | stmt SEMICOLON stmts_plus
newline_star ::=   /* empty */ | NEWLINE newline_star
stmt ::=  newline_star compound_stmt | newline_star small_stmt
small_stmt ::=  assignment | star_exps | RETURN star_exps | PASS | ASSERT exp | BREAK
compound_stmt ::=  list DEF IDENTIFIER LPAREN param_star RPAREN ARROW typ_id COLON block | IF exp COLON block elif_star ELSE COLON block | IF exp COLON block elif_star | list FOR star_targets IN star_exps COLON block | list WHILE exp COLON block
assignment ::=  exp COLON exp EQ star_exps | exp EQ star_exps | exp PLUSEQ star_exps | exp MINUSEQ star_exps | exp TIMESEQ star_exps | exp DIVIDEEQ star_exps
elif_star ::=   /* empty */ | ELIF exp COLON block elif_star
star_exps ::=  exp star_exps_rest COMMA | exp star_exps_rest | exp COMMA | exp
star_exps_rest ::=  star_exps_rest COMMA exp | COMMA exp
star_targets ::=  star_target star_targets_rest COMMA | star_target star_targets_rest | star_target
star_targets_rest ::=  star_targets_rest COMMA star_target | COMMA star_target
star_target ::=  IDENTIFIER | LPAREN star_targets RPAREN | LBRACK star_targets RBRACK
exp ::=  implication IF implication ELSE exp | LAMBDA id_star COLON exp | implication | typ
implication ::=  implication BIIMPL disjunction | implication IMPLIES disjunction | implication EXPLIES disjunction | disjunction
disjunction ::=  disjunction OR conjunction | conjunction
conjunction ::=  conjunction AND inversion | inversion
inversion ::=  NOT inversion | comparison
comparison ::=  comparison EQEQ sum | comparison NEQ sum | comparison LTE sum | comparison LT sum | comparison GTE sum | comparison GT sum | comparison NOT_IN sum | comparison IN sum | sum
sum ::=  sum PLUS term | sum MINUS term | term
term ::=  term TIMES factor | term DIVIDE factor | term MOD factor | factor
factor ::=  PLUS factor | MINUS factor | power
power ::=  primary
primary ::=  primary DOT IDENTIFIER | primary LPAREN arguments RPAREN | primary slice | atom
arguments ::=  exp_star
atom ::=  IDENTIFIER | TRUE | FALSE | INT | FLOAT | strings | NONE | FORALL id_star DOUBLECOLON exp | EXISTS id_star DOUBLECOLON exp | LPAREN exp COMMA exp_star RPAREN | LPAREN exp RPAREN | lst_exp | set_exp | dict_exp | LEN LPAREN star_exps RPAREN | MAX LPAREN star_exps RPAREN | OLD LPAREN star_exps RPAREN | FRESH LPAREN star_exps RPAREN
strings ::=  STRING | strings STRING
slice ::=  LBRACK exp COLON exp RBRACK | LBRACK exp COLON RBRACK | LBRACK COLON exp RBRACK | LBRACK COLON RBRACK | LBRACK exp RBRACK
lst_exp ::=  LBRACK exp_star RBRACK
dict_exp ::=  LBRACE kv_star RBRACE
kv_star ::=   /* empty */ | kv_rest
kv_rest ::=  kv COMMA kv_rest | kv COMMA | kv
kv ::=  exp COLON exp
set_exp ::=  LBRACE exp_star RBRACE
spec ::=  PRE spec_rem | POST spec_rem | DECREASES spec_rem | INVARIANT spec_rem | READS spec_rem | MODIFIES spec_rem
spec_rem ::=  exp NEWLINE
block ::=  NEWLINE newline_star indent_plus stmts_plus dedent_plus
indent_plus ::=  INDENT
dedent_plus ::=  DEDENT
typ_id ::=  typ | IDENTIFIER
typ ::=  data_typ | base_typ
typ_plus ::=  typ_plus COMMA typ_id | typ_id
base_typ ::=  STRING_TYP | INT_TYP | FLOAT_TYP | BOOL_TYP | NONE | OBJ_TYP
data_typ ::=  LIST_TYP LBRACK typ_id RBRACK | LIST_TYP | DICT_TYP LBRACK typ_id COMMA typ_id RBRACK | DICT_TYP | SET_TYP LBRACK typ_id RBRACK | SET_TYP | TUPLE_TYP LBRACK typ_plus RBRACK | TUPLE_TYP | CALLABLE_TYP LBRACK LBRACK typ_plus RBRACK COMMA typ_id RBRACK | TYPE_TYP LBRACK typ_id RBRACK | TYPE_TYP
param_star ::=   /* empty */ | param_rest
param_rest ::=  param COMMA param_rest | param COMMA | param
param ::=  IDENTIFIER COLON exp
id_star ::=  /* empty */ | id_rest
id_rest ::=  IDENTIFIER COMMA id_rest | IDENTIFIER
exp_star ::=   /* empty */ | exp_rest
exp_rest ::=  exp COMMA exp_rest | exp COMMA | exp

// Tokens

//comment lexbuf  ::= "import"
//comment lexbuf  ::= "from"
FORALL  ::= "forall"
EXISTS  ::= "exists"
BIIMPL  ::= "<==>"
IMPLIES  ::= "==>"
EXPLIES  ::= "<=="
DOUBLECOLON  ::= "::"
LPAREN  ::= '('
RPAREN  ::= ')'
LBRACE  ::= '{'
RBRACE  ::= '}'
LBRACK  ::= '['
RBRACK  ::= ']'
DOT  ::= '.'
COLON  ::= ':'
SEMICOLON  ::= ';'
COMMA  ::= ','
OLD  ::= "old"
LEN  ::= "len"
IDENTIFIER  ::= "max"
IDENTIFIER  ::= "filter"
IDENTIFIER  ::= "map"
ARROW  ::= "->"
ARROW  ::= "->"
DEF  ::= "def"
LAMBDA  ::= "lambda"
IF  ::= "if"
ELIF  ::= "elif"
ELSE  ::= "else"
FOR  ::= "for"
WHILE  ::= "while"
BREAK  ::= "break"
PASS  ::= "pass"
RETURN  ::= "return"
ASSERT  ::= "assert"
NOT_IN  ::= "not in"
IN  ::= "in"
EQEQ  ::= "=="
EQ  ::= '='
NEQ  ::= "!="
PLUS  ::= '+'
PLUSEQ  ::= "+="
MINUS  ::= '-'
MINUSEQ  ::= "-="
TIMES  ::= '*'
TIMESEQ  ::= "*="
DIVIDE  ::= "/"
DIVIDEEQ  ::= "/="
MOD  ::= "%"
LTE  ::= "<="
LT  ::= '<'
GTE  ::= ">="
GT  ::= '>'
AND  ::= "and"
OR  ::= "or"
NOT  ::= "not"
TRUE  ::= "True"
FALSE  ::= "False"
NONE  ::= "None"

Issue with mehir library?

Hi, I'm very interested in using your work to translate some python code into Dafny. Cool work! I'm struggling to get the system working locally, though. I am using menhir version 2.0 since 2.1 was for some reason not supported for me, and I'm seeing this error

Any advice?

Many thanks in advance.