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 - DC 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
