[m-users.] A more precise determinism checker
dirk at ziegemeyer.de
Wed Mar 23 01:47:25 AEDT 2022
> Am 19.03.2022 um 17:12 schrieb Philip White <philip at pswhite.org>:
> I'd love to hear what people think of this approach. I haven't yet
> tested it at large scale with huge predicates, so my biggest concern is
> that it will be really, really slow.
Mercury's determinism checker works fine for about 90 percent of my predicates. I wish there would exist some solution to assist Mercury with the remaining 10 percent.
A pattern that happens very frequently to me: I know exactly that a key is not a member of the keys of a map. Inserting this key into the map under this precondition (with map.insert/4) is of determinism det instead of semidet.
Maybe this is a source of inspiration for your project:
"LiquidHaskell (LH) refines Haskell's types with logical predicates that let you enforce important properties at compile time." (from their homepage).
It uses an SMT-LIB solver (e.g. Z3).
The Z3 solver is also used by SPARK/Ada.
More information about the users