Re: failure of formal verification [software.imdea.org] (Was: The issue with free speech)

So what is the spec. Well one can use:
Red-Black Trees in a Functional Setting
https://www.cs.tufts.edu/~nr/cs257/archive/chris-okasaki/redblack99.pdf
insert :: (Ord a) => a -> Tree a -> Tree a
insert x s = makeBlack $ ins s
   where ins E  = T R E x E
         ins (T color a y b)
           | x < y  = balance color (ins a) y b
           | x == y = T color a y b
           | x > y  = balance color a y (ins b)
         makeBlack (T _ a y b) = T B a y b
The balancing would be as follows, again Haskell code:
balance :: Color -> Tree a -> a -> Tree a -> Tree a
balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
balance color a x b = T color a x b
Does SWI-Prolog implement somewhere Okasaki red-black trees.
Mild Shock schrieb:

Hi,
 Not only are the fucking PIPs behind a
login wall that doesn't work:
 Dictionaries in Prolog
https://gitlab.software.imdea.org/prolog-lang/pip-0102
 I cannot read gitlab.software.imdea.org,
since it redirects to some internal server
during login.
 Also formal verification doesn't have the
same track record as fuzzying. Take the SWI-Prolog
red-black trees. Are they really red-black trees?
 I used fuzzy testing to find the test case.
Exhaustive enumeration of permutation seemed to
be out of reach computationally.
 So I used these random permutations to find a
discrepancy in resulting tree depth:
 fuzzer(R) :-
    numlist(1, 16, L),
    between(1, 1000, _),
    random_permutation(L, R).
 Maybe the same technique can use to find smaller
discrepancies, and then use the smaller examples to
pin down difference in implemented balance
 rules or implement rebalancing strategy.
 Bye
 Mild Shock schrieb:

@herme wrote:
>
Just a quick comment: note that you can make
and discuss the PIP proposals directly on
the PIPs discourse.
>
Here my response:
>
I will probably never go there since somebody
tried censoring my comments and said I don’t
work towards the Prolog cause. The good thing
about SWI-Prolog discourse, it has become
>
quite calm cocerning attempts to censor people,
possibly because some particular people left.
Which is in my opinion the best thing that
could happen to this forum. There is no
>
guarantee in other forums to really have free speech.
>