I've recently prepared an extension to the contract system based on some work that Cormac Flanagan and I did.
The code is available at: https://github.com/jeapostrophe/exp/tree/master/temporal-ctcs The documentation is available at: http://faculty.cs.byu.edu/~jay/tmp/20110107-tempc/temp-c/ and http://faculty.cs.byu.edu/~jay/tmp/20110107-tempc/automata/ Here is a short example: (with-monitor (cons/c (label 'malloc (-> addr?)) (label 'free (-> addr? void?))) (complement (seq (star _) (dseq (call 'free addr) (seq (star (not (ret 'malloc (== addr)))) (call 'free (== addr))))))) This creates a contract for a pair of functions, malloc and free, where the contract system ensures the malloc always returns addresses and free takes address and returns void. Additionally, the monitoring system ensures that the only legal interactions between these functions and their clients are those that do not end in a double free (a free followed by a free without a malloc of the same address in between.) Should this code be a PLaneT package or should it go into the core? I think it is quite a big extension over racket/contract. What do you think generally? Jay -- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.cs.byu.edu/~jay "The glory of God is Intelligence" - D&C 93 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
