[racket-dev] Temporal Contracts and Match Automata

From: Jay McCarthy (jay.mccarthy at gmail.com)
Date: Fri Jan 7 20:17:16 EST 2011

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:


The documentation is available at:




Here is a short example:

      (cons/c (label 'malloc (-> addr?))
              (label 'free (-> addr? void?)))
     (seq (star _)
          (dseq (call 'free addr)
                 (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

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

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

Posted on the dev mailing list.