gdp: Reason about invariants and preconditions with ghosts of departed proofs.
Reason about invariants and preconditions with ghosts of departed proofs.
The GDP library implements building blocks for creating and working with
APIs that may carry intricate preconditions for proper use. As a library
author, you can use gdp
to encode your API's preconditions and invariants,
so that they will be statically checked at compile-time.
As a library user, you can use the gdp
deduction rules to codify your
proofs that you are using the library correctly.
[Skip to Readme]
Modules
[Index] [Quick Jump]
Downloads
- gdp-0.0.3.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.0.0.1, 0.0.0.2, 0.0.3.0 |
---|---|
Dependencies | base (>=4.7 && <5), gdp, lawful [details] |
License | BSD-3-Clause |
Copyright | (c) 2018 Matt Noonan |
Author | Matt Noonan |
Maintainer | matt.noonan@gmail.com |
Category | Safe |
Home page | https://github.com/matt-noonan/gdp#readme |
Source repo | head: git clone https://github.com/matt-noonan/gdp |
Uploaded | by mnoonan at 2019-11-13T00:39:06Z |
Distributions | LTSHaskell:0.0.3.0, NixOS:0.0.3.0, Stackage:0.0.3.0 |
Reverse Dependencies | 4 direct, 7 indirect [details] |
Executables | gdp |
Downloads | 2072 total (20 in the last 30 days) |
Rating | 2.25 (votes: 2) [estimated by Bayesian average] |
Your Rating | |
Status | Docs available [build log] Last success reported on 2019-11-13 [all 1 reports] |