|
|
|
# verify-elm
|
|
|
|
|
|
|
|
## Idea
|
|
|
|
|
|
|
|
Translate Elm code and properties into SMT in order to verify frontend-related
|
|
|
|
programs.
|
|
|
|
|
|
|
|
* SMT translation (of Elm code and properties) and SMT communication
|
|
|
|
* integration with/reusage of property-based testing library
|
|
|
|
* implementation of exemplary Elm applications
|
|
|
|
* tooling support for verification process that documents (successful) translations and SMT answers
|
|
|
|
|
|
|
|
## Schedule
|
|
|
|
|
|
|
|
1. Learning Elm by developing simple example programs
|
|
|
|
2. Formalizing properties of the developed programs and creating pre- and postconditions
|
|
|
|
3. Creating simple examples to get to know SMT solvers
|
|
|
|
4. Using Haskell to get hook up into the elm compile process
|
|
|
|
5. Generate SMT using the pre- and postconditions and the given elm program
|
|
|
|
6. Develop tooling
|
|
|
|
7. ...
|
|
|
|
|
|
|
|
## Elm
|
|
|
|
|
|
|
|
Elm is a functional, statically typed programming language that compiles to JavaScript and,
|
|
|
|
thus, enables the user to write functional code for the web browser.
|
|
|
|
|
|
|
|
## Background
|
|
|
|
[VerifiedReact](https://github.com/aestheticIntegration/verified-react) is an
|
|
|
|
ongoing project that translated [ReasonML](https://reasonml.github.io) code and
|
|
|
|
properties into SMT to verify frontend components. ReasonML is a functional, statically
|
|
|
|
typed programming language based on Ocaml, the functional paradigm and type information
|
|
|
|
ease the task of transforming such programs to SMT.
|
|
|
|
[A recent blog post](https://medium.com/imandra/verifying-reasonreact-component-logic-reasonml-imandra-e350d4812a9f)
|
|
|
|
describes the first efforts to develop a tool that verifies properties of a
|
|
|
|
TicTacToe implementation in ReasonML.
|
|
|
|
|
|
|
|
## Links
|
|
|
|
|
|
|
|
### Useful tooling for Elm
|
|
|
|
|
|
|
|
* [elm-compiler-docs](https://github.com/elm-community/elm-compiler-docs): unofficial documentation of the Elm compiler
|
|
|
|
* [elm-ast](https://github.com/Bogdanp/elm-ast/tree/8.0.12): a parser for Elm in Elm
|
|
|
|
* [elm-analyse](https://github.com/stil4m/elm-analyse): a tool for (static) analyses of Elm code
|
|
|
|
* [elm-check](https://github.com/TheSeamau5/elm-check): library for property-based testing in Elm
|
|
|
|
* [language-elm](https://github.com/eliaslfox/language-elm): a Haskell library for generating Elm source code from an ast
|
|
|
|
* [elm-compiler](https://github.com/elm/compiler): the Elm compiler written in Haskell
|
|
|
|
* [elm-compiler-tooling](https://github.com/elm-tooling/elm-compiler-library): a library version of the Elm compiler
|
|
|
|
|
|
|
|
### SMT
|
|
|
|
|
|
|
|
* [sbv](http://leventerkok.github.io/sbv/): SMT library for Haskell
|
|
|
|
* [TIP](http://tip-org.github.io): project that translates Haskell programs into an intermediate language TIP
|
|
|
|
* [A gentle introduction to symbolic execution](https://blog.monic.co/a-gentle-introduction-to-symbolic-execution/): a blog post about symbolic execution of Haskell programs
|
|
|
|
* [SAT/SMT by Example](https://yurichev.com/SAT_SMT.html): free (open source) book about SAT and SMT
|
|
|
|
* [Z3 SMT-Solver](https://github.com/Z3Prover/z3) |
