typeCart is an analysis tool for proof evolution to facilitate proof maintenance for continuously integrated software. typeCart is constructed in F# and it
- reads two Dafny files into Dafny AST,
- analyses the ASTs to identify syntactically equivalent types between them, and
- generates mapping functions between equivalent types.
Additionally, typeCart generates the verification contracts (Dafny's require and ensure clauses) for the mapping functions, enabling the Dafny verifier to successfully verify the generated functions. Such functions helps proof engineers in estimating a quantitative measure about incremental changes between two version of the same specs written in Dafny.
Trivia: Cart in typeCart represents cartography: typeCart generates mapping functions for equal types.
typeCart builds on .NET 5.0, it supports Dafny 3.3.0 and Z3 4.8.5. The Makefile is configured to install Dafny and Z3 locally in the root directory. After installing .NET 5.0, run in the root directory
> make
to build the project.
To run tests, use
> make test
Other make options: deps, check_format, clean
Contributions are welcomed! See CONTRIBUTING guidelines for more information.
typeCart is distributed under MIT license, see LICENSE.txt for details.