Difference between revisions of "Liquid Haskell"

From HaskellWiki
Jump to navigation Jump to search
(link to Blog)
(Update links)
Tag: visualeditor-switched
 
Line 1: Line 1:
Liquid Haskell allows to annotate code with invariants
+
Liquid Haskell allows to annotate code with specifications
that complement the invariants imposed by the types.
+
that complement the validation imposed by the types.
These invariants are checked with an SMT solver.
+
These specifications are checked with an SMT solver.
Such invariants may be non-negative numbers, sorted lists, matching lengths of lists, membership of certain elements in a <hask>Set</hask> or <hask>Map</hask>.
+
They can check for non-negative numbers, sorted lists, matching lengths of lists, membership of certain elements in a <hask>Set</hask> or <hask>Map</hask>, and [https://ucsd-progsys.github.io/liquidhaskell/papers/ more].
   
  +
  +
* [https://ucsd-progsys.github.io/liquidhaskell/ Documentation]
 
* [https://github.com/ucsd-progsys/liquidhaskell/ GitHub]
 
* Hackage: {{HackagePackage|id=liquidhaskell}}
 
* Hackage: {{HackagePackage|id=liquidhaskell}}
* [http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/ Blog]
 
* [http://goto.ucsd.edu/liquidhaskell Online demo]
 
   
 
== See also ==
 
== See also ==
   
 
* [[Catch]]
 
* [[Catch]]
* [[ESC]]
+
* [[Extended_Static_Checking|ESC]]
   
 
[[Category:Development tools]]
 
[[Category:Development tools]]

Latest revision as of 13:58, 16 July 2023

Liquid Haskell allows to annotate code with specifications that complement the validation imposed by the types. These specifications are checked with an SMT solver. They can check for non-negative numbers, sorted lists, matching lengths of lists, membership of certain elements in a Set or Map, and more.


See also