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 [RSS]||0.0.0.1, 0.0.0.2, 0.0.3.0|
|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 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]|
|Downloads||1757 total (20 in the last 30 days)|
|Rating||2.0 (votes: 1) [estimated by Bayesian average]|
|Status||Docs available [build log]
Last success reported on 2019-11-13 [all 1 reports]