add counter examples to rbtrees

This commit is contained in:
Robby Findler 2014-03-19 14:12:47 -05:00
parent a451fcfa47
commit 09d78f0604
6 changed files with 47 additions and 0 deletions

View File

@ -10,3 +10,10 @@
< (balance (c t_1 n_2 (ins n_1 t_2))) < (balance (c t_1 n_2 (ins n_1 t_2)))
--- ---
> (c t_1 n_2 (ins n_1 t_2)) > (c t_1 n_2 (ins n_1 t_2))
301a302,307
> (define small-counter-example
> (term (B (R E (num->n 0) E)
> (num->n 2)
> E)))
> (test-equal (check small-counter-example) #f)
>

View File

@ -5,3 +5,10 @@
100,101d99 100,101d99
< [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4)) < [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4))
< (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))] < (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
301a300,305
> (define small-counter-example
> (term (B (R E (num->n 1) E)
> (num->n 2)
> E)))
> (test-equal (check small-counter-example) #f)
>

View File

@ -6,3 +6,14 @@
< [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd)) < [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd))
--- ---
> [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max n_bd) > [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max n_bd)
301a302,311
> (define small-counter-example
> (term (B
> (B
> (R E (num->n 1) E)
> (num->n 2)
> (R E (num->n 3) E))
> (num->n 4)
> (R E (num->n 5) E))))
> (test-equal (check small-counter-example) #f)
>

View File

@ -299,6 +299,12 @@
(generate-term rbtrees t #:i-th index) (generate-term rbtrees t #:i-th index)
(set! index (add1 index)))))) (set! index (add1 index))))))
(define small-counter-example
(term (B (R E (num->n 0) E)
(num->n 2)
E)))
(test-equal (check small-counter-example) #f)
(define fixed (define fixed
(term (term
(;; 1 and 2 (;; 1 and 2

View File

@ -297,6 +297,12 @@
(generate-term rbtrees t #:i-th index) (generate-term rbtrees t #:i-th index)
(set! index (add1 index)))))) (set! index (add1 index))))))
(define small-counter-example
(term (B (R E (num->n 1) E)
(num->n 2)
E)))
(test-equal (check small-counter-example) #f)
(define fixed (define fixed
(term (term
(;; 1 and 2 (;; 1 and 2

View File

@ -299,6 +299,16 @@
(generate-term rbtrees t #:i-th index) (generate-term rbtrees t #:i-th index)
(set! index (add1 index)))))) (set! index (add1 index))))))
(define small-counter-example
(term (B
(B
(R E (num->n 1) E)
(num->n 2)
(R E (num->n 3) E))
(num->n 4)
(R E (num->n 5) E))))
(test-equal (check small-counter-example) #f)
(define fixed (define fixed
(term (term
(;; 1 and 2 (;; 1 and 2