search

vdimir / py-refinement-lambda

Pyrefine – python code checker based on Hoare logic
9 stars 0 forks source link

I came across this repo. Can you describe this project a bit more? #1

Open simkimsia opened 5 years ago

simkimsia commented 5 years ago

Hi there,

I recently learned about hoare triple and googled "Hoare Logic Visual Studio Code" thinking maybe someone figured out a way to include hoare triple as a way to check for correctness in code in visual studio code.

That's how I found this project. Your project looks interesting, though I admit I'm out of my depth. I don't really grok the "why" behind this project. So if you be so kind to help me better understand why and how this pyrefinement is useful to developers. That would be great.

Thank you 🙏

vdimir commented 5 years ago

Hi,

I develop this tool within my master thesis. In few words it builds logical equations for your program statements and checks it using Z3 SMT solver.

Actually, it is small proof of concept and cannot be used for real-world programs now. You can see examples of programs in examples folder in repo but all of them not so complex.

I have pdf with text of my thesis, but it is in Russian and I don't think it helps you. List of references can be useful (I upload it here). Not all references contains links but you can find it googling by title.

Also I recommend to look at LiquidHaskell. I was inspired by this tool, but you should be familiar with Haskell. During research I have found experimental language Dafny developed by Microsoft with similar idea.

If you have other questions we can discuss it. Also you can email me to vcherckasov@yandex.ru