learning how to use MrSpidey

[Marco Maggesi <maggesi@math.unifi.it>]

Hi,

I am new to the use of PLT MrSpidey (I just installed it) and I am
trying to learn how it works, and how to take the best of it.  I used
this small program as test

  01: (define (add x y)
  02:   (cond ((and (number? x) (number? y))
  03:          (+ x y))
  04:         ((and (list? x) (list? y))
  05:          (append x y))
  06:         (else
  07:          (error "Invalid input" x y add))))
  08: 
  09: (define (neg x)
  10:   (if (number? x)
  11:       (- x)
  12:       (if (list? x)
  13:           (map neg x)
  14:           (error "Invalid input" x neg))))
  15: 
  16: (add 2 4)
  17: (add (list 1 2 3) (list 4 5))
  18: (add 3 (list 0 1))
  19: 
  20: (neg 3)
  21: (neg (list 1 2))
  22: (neg (vector 1 2 3))

I would like to understand if MrSpidey is capable to reveal the
following facts:

  (1)  Both the expressions at line 16 and 20 will return a number.

  (2)  Both the expressions at line 17 and 21 will return a list.

  (3)  Both the expressions at line 18 and 22 will cause an error
       (because of the error call at line 07 and 14 respectively).

I would expect that (1) and (2) were possible, but it seems that
MrSpidey simply notice that both number and list are possible type as
return value.  Is a better analysis possible?

Is it possible (perhaps adding some more information in the code) to make
MrSpidey notice (3) also?

Thanks, MM