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
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.
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
/needn't be escaped.
TypeInjections/TypeInjections.Test: Tests for typeCart
TypeInjections/Tool: dotnet CLI tool for typeCart.
typeCart takes as input two Dafny files or folders, and generates the analysis results into a folder.
Following is the command to run the
complex example and output the result into the
To run typeCart on the commit history of Cedar's Dafny specification:
typeCart may generate code that is not automatically verifiable by Dafny. See Troubleshooting.
Contributions are welcomed! See CONTRIBUTING guidelines for more information.
typeCart is distributed under MIT license, see LICENSE.txt for details.