Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/awslabs/typecart

https://github.com/awslabs/typecart

Science Score: 13.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ○
    .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (11.5%) to scientific vocabulary
Last synced: 9 months ago · JSON representation

Repository

Basic Info
  • Host: GitHub
  • Owner: awslabs
  • License: other
  • Language: Dafny
  • Default Branch: main
  • Size: 1.98 MB
Statistics
  • Stars: 22
  • Watchers: 7
  • Forks: 8
  • Open Issues: 1
  • Releases: 1
Created over 4 years ago · Last pushed over 1 year ago
Metadata Files
Readme Contributing License Code of conduct

README.md

TypeCart

.NET build

typeCart is an analysis tool for proof evolution to facilitate proof maintenance for continuously integrated software. typeCart is constructed in F# and it

  1. reads two Dafny files into Dafny AST,
  2. analyses the ASTs to identify syntactically equivalent types between them, and
  3. 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.

See examples and features.

Build

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 typeCart
  • TypeInjections/Tool: dotnet CLI tool for typeCart.

Run

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 tmp folder:

shell TypeInjections/TypeInjections/bin/Debug/net6.0/TypeInjections \ examples/complex/old.dfy \ examples/complex/new.dfy \ tmp

To run typeCart on the commit history of Cedar's Dafny specification: shell cd scripts bash run_cedar.sh

Troubleshooting

typeCart may generate code that is not automatically verifiable by Dafny. See Troubleshooting.

Contributing

Contributions are welcomed! See CONTRIBUTING guidelines for more information.

License

typeCart is distributed under MIT license, see LICENSE.txt for details.

Owner

  • Name: Amazon Web Services - Labs
  • Login: awslabs
  • Kind: organization
  • Location: Seattle, WA

AWS Labs

GitHub Events

Total
  • Watch event: 2
  • Issue comment event: 2
  • Push event: 5
  • Pull request review event: 2
  • Pull request event: 6
  • Fork event: 1
Last Year
  • Watch event: 2
  • Issue comment event: 2
  • Push event: 5
  • Pull request review event: 2
  • Pull request event: 6
  • Fork event: 1

Issues and Pull Requests

Last synced: 11 months ago

All Time
  • Total issues: 2
  • Total pull requests: 34
  • Average time to close issues: 5 months
  • Average time to close pull requests: 2 days
  • Total issue authors: 2
  • Total pull request authors: 8
  • Average comments per issue: 1.0
  • Average comments per pull request: 0.5
  • Merged pull requests: 28
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 5
  • Average time to close issues: N/A
  • Average time to close pull requests: about 12 hours
  • Issue authors: 0
  • Pull request authors: 2
  • Average comments per issue: 0
  • Average comments per pull request: 0.2
  • Merged pull requests: 3
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
  • mschlaipfer (1)
  • seanmcl (1)
Pull Request Authors
  • tschuerl (13)
  • ruijiefang (7)
  • hirataqdees (6)
  • xumingkuan (4)
  • rifatarefin (2)
  • mschlaipfer (1)
  • joscoh (1)
  • seanmcl (1)
  • akravc (1)
Top Labels
Issue Labels
v1-issue (1)
Pull Request Labels

Packages

  • Total packages: 1
  • Total downloads:
    • nuget 3,684 total
  • Total dependent packages: 0
  • Total dependent repositories: 0
  • Total versions: 6
  • Total maintainers: 1
nuget.org: typecart

Package Description

  • License: other
  • Latest release: 1.0.5
    published almost 4 years ago
  • Versions: 6
  • Dependent Packages: 0
  • Dependent Repositories: 0
  • Downloads: 3,684 Total
Rankings
Dependent repos count: 12.7%
Dependent packages count: 19.5%
Average: 22.8%
Downloads: 36.1%
Maintainers (1)
tschuerl
Last synced: 9 months ago

Dependencies

.github/workflows/dotnet.yml actions
  • actions/checkout v2 composite
  • actions/setup-dotnet v1 composite