Static analysis of signed integer addition and multiplication in Racket (see http://matt.might.net/articles/intro-static-analysis/)

abstract-integers.rkt

#lang racket

(require racket/set)

; elements in the abstract integers
(define S (set '+ 'o '-))

; Z -> S
(define (alpha z)
  (cond
    ((< z 0) '-)
    ((= z 0) 'o)
    ((> z 0) '+)))

; addition table for S
(define singleton-add (make-hash))
(hash-set! singleton-add (set '- '-) (set '-))
(hash-set! singleton-add (set '- '+) (set '- 'o '+))
(hash-set! singleton-add (set '- 'o) (set '-))
(hash-set! singleton-add (set '+ 'o) (set '+))
(hash-set! singleton-add (set '+ '+) (set '+))
(hash-set! singleton-add (set 'o 'o) (set 'o))

; multiplication table for S
(define singleton-mult (make-hash))
(hash-set! singleton-mult (set '- '-) (set '+))
(hash-set! singleton-mult (set '- '+) (set '-))
(hash-set! singleton-mult (set '- 'o) (set 'o))
(hash-set! singleton-mult (set '+ 'o) (set 'o))
(hash-set! singleton-mult (set '+ '+) (set '+))
(hash-set! singleton-mult (set 'o 'o) (set 'o))

; m and n are powersets of S; h is a hash table mapping all non-trivial
; powersets of S (cardinality /= 0 and cardinality /= |S|) to non-empty
; powersets of S
(define (combine h m n)
  (if (or (set-empty? m) (set-empty? n))
    (set) ; empty set
    (foldl set-union (set) (set->list (for*/set ([a m] [b n])
        (hash-ref h (set a b))))))) ; union of all combinations looked up in h

; "add" two sets of operators
(define (add x y) (combine singleton-add x y))

; calculate the bound on the sign from adding two integers
(define (z-add x y)
  (add (set (alpha x)) (set (alpha y))))

; "multiply" two sets of operators
(define (mult x y) (combine singleton-mult x y))

; calculate the bound on the sign from multiplying two integers
(define (z-mult x y)
  (mult (set (alpha x)) (set (alpha y))))