[racket-dev] Temporal Contracts and Match Automata

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 <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93