[racket-dev] Temporal Contracts and Match Automata

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 <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
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/dev