Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock Newsgroups: comp.lang.prolog Subject: Re: failure of formal verification [software.imdea.org] (Was: The issue with free speech) Date: Wed, 6 Nov 2024 09:35:17 +0100 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Wed, 6 Nov 2024 08:35:16 -0000 (UTC) Injection-Info: solani.org; logging-data="590884"; mail-complaints-to="abuse@news.solani.org" User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.19 Cancel-Lock: sha1:nAFf9P/bADexUDQQrhB1Cd2i0gE= X-User-ID: eJwNyMEBwCAIA8CVRCDAOBFl/xHae54rBB0Gh/n4GPiEHWpZV+7O5YtdMQdKWYqz2dAu6p7KcEr/9WLM+K58TN8VsA== In-Reply-To: Bytes: 3835 Lines: 84 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. >> >