In principle I'd love to see this kind of functionality in the core. I will read the 'guide' (aka your submission) and let's work on my 'turn' example to see how it fits.
-- Matthias On Jan 7, 2011, at 8:17 PM, Jay McCarthy wrote: > 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 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev