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]
|Versions [faq]||0.0.0.1, 0.0.0.2|
|Dependencies||base (>=4.7 && <5), gdp, lawful [details]|
|Copyright||(c) 2018 Matt Noonan|
|Source repo||head: git clone https://github.com/matt-noonan/gdp|
|Uploaded||by mnoonan at Mon Jun 18 02:02:57 UTC 2018|
|Distributions||LTSHaskell:0.0.0.2, NixOS:0.0.0.2, Stackage:0.0.0.2|
|Downloads||257 total (47 in the last 30 days)|
|Rating||(no votes yet) [estimated by rule of succession]|
Docs available [build log]
Last success reported on 2018-06-18 [all 1 reports]
For package maintainers and hackage trustees