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 6.0. To build typeCart, simply invoke dotnet build
in the following three project folders:
TypeInjections/TypeInjections
: Main typeCart program. To use typeCart, run the compiled program on two dafny files, two directories containing a dafny project each, with an optional argument being a list of regex dictating what files typeCart should ignore in the directory. The regexes would match on the ignored filenames, and.
and/
needn't be escaped.TypeInjections/TypeInjections.Test
: Tests for typeCartTypeInjections/Tool
: dotnet CLI tool for typeCart.
Contributions are welcomed! See CONTRIBUTING guidelines for more information.
typeCart is distributed under MIT license, see LICENSE.txt for details.