Paul,
it sounds to me like what you really want is an analysis tool that can validate claims or perhaps synthesize (valid) properties from programs in your specification and implementation languages. As Jonathan says (indirectly), that's not really what Redex is for. If you had an analysis that validates/synthesizes claims about the relationship between specifications and implementations, you could build a Redex model to verify the meta-theorem about your analysis. If you had a Redex model of your implementation language, you could derive a CFA from it using the Redex book and DVH's AAM method. I doubt that this flow analysis would be useful to validate the kind of claims you are thinking about. >From the little that I know about your work (previous draft paper), I could imagine that mapping your specs into a software modeler such as Alloy might help you state and refute/validate such claims. But as I say, this is a conjecture. -- Matthias On Mar 31, 2015, at 12:23 PM, Jonathan Schuster <[email protected]> wrote: > Forgot to reply to the list, so I'm forwarding here. > > ---------- Forwarded message ---------- > From: Paul van der Walt <[email protected]> > Date: Tue, Mar 31, 2015 at 12:06 PM > Subject: Re: [racket-users] Using Redex > To: Jonathan Schuster <[email protected]> > > > Hi Jonathan, > > Thanks for your response! I'm not sure if it'd be beneficial to cc: the > mailing list, feel free to forward if excluding the ML wasn't > intentional on your part. > > On 2015-03-31 at 17:44, quoth Jonathan Schuster: > > Paul, my initial reaction is that this sounds like an odd use of Redex. > > Right. I was starting to get this suspicion too, as i went along with > reading The Book and the tutorials available, etc. > > > Using your language terms to define implement-* macros is a valid > > implementation strategy, > > Nice as a reality check indeed :) > > > but as a formal semantics it differs from the typcial Redex > > approach. > > Yeah indeed. Notably the fact that the "image" of my language > transformation is not the same as its domain makes me uneasy. > > What might have been possible is to model the output (that is, find an > abstraction of defining macros etc) and have redex to that > transformation. That way, the gap between what i eventually do in the > implementation and the redex model is smaller. But it looks like > actually i need to find an abstraction which is closer to the domain > (the specification language). > > I guess in my case i should come up with some sort of > mathematical/abstract model of the resulting components (e.g. a directed > graph of communicating nodes) so that i can use that to prove properties > (e.g. node A and B communicate iff that's in the specification terms). > > > It might be the case that Redex can help you develop a > > separate formal semantics, though. Perhaps others on this list have > > other thoughts or suggestions. > > Yeah, that is basically what i think i would like to do now, as a lite™ > version of what i was trying to do. Or perhaps try and formalise one or > two core components of my runtime system (but i'm less clear on how i > could approach that. > > > Since you already have a working prototype, can I ask what benefit you're > > hoping to get from Redex? There are certainly a number of possibilities, > > but it depends on your goals. > > Mainly i would like to be able to make strong statements, such as > "communication between component C1 and C2 is impossible, since they are > independent in the specification". Currently i can argue that looking at > the specifications of a set of components, but it becomes hand-wavey in > the implementation -- i cannot *really* guarantee that there is no > out-of-band communication except via intuitive arguments... > > Thank you very much for your comments! > > p. > > > > On Sat, Mar 28, 2015 at 12:58 PM, Paul van der Walt < > > [email protected]> wrote: > > > >> Hello Racketeers, > >> > >> TLDR: I want to implement [1] using Redex. > >> > >> I hope somebody can shed some light on my problem. I'm trying to use > >> Redex (which looks super cool, but i'm having trouble wrapping my head > >> around all of it), and i'm a little stuck (i've tried RTFM, but i'm a > >> little lost anyway). I wonder if what i'm trying to do is > >> reasonable/feasible. > >> > >> I have a system which works, which i want to "reimplement" using Redex. > >> My system (already in Racket) does the following: it provides a > >> declaration language (just a set of keywords which aren't particularly > >> relevant to the problem) which can be used to specify separate > >> components expected in an application. It provides keywords like > >> > >> #lang myspeclang > >> (define-component SomeName Int) ; declare a component > >> > >> This file should then be referred to by the "implementation module", so > >> if the above is written in a file called specs.rkt, i provide a > >> mechanism to write the following sort of terms: > >> > >> #lang "specs.rkt" > >> (implement-SomeName (lambda () .....)) ; provide SomeName's implementation > >> > >> This is done by various macro tricks (nothing groundbreaking) -- i > >> provide macros like the implement-SomeName above, depending on the > >> declarations provided. > >> > >> Anyway, i am beginning to wonder if this type of thing can be expressed > >> in Redex? I have a Redex model which specifies the grammar of my > >> declarations, which i use to evaluate the declarations (thanks to David > >> van Horn's approach [0]). I can see this working, but ultimately i'm not > >> actually interested in a reduction relation per se: the declarations are > >> already "reduced" and i'm interested in them only for their > >> side-effects, e.g. defining a macro called "implement-SomeName" when a > >> declaration for SomeName is encountered. I've been toying with this > >> idea, and i'm worried i'd have to model (minimal) Racket itself in Redex > >> to be able to express what these declarations should reduce to, but that > >> (intuitively) sounds like the Wrong Way™ to go about things. My other > >> idea was to add a "skip" terminal to the declaration language which > >> everything reduces to, but as a side-effect running a bunch of code to > >> define the needed macros. This also sounds Ugly©, though. Basically, my > >> reduction goes from the domain of my declarations to the domain of > >> macros or modules, and not, like in the schoolbook λ-calculus examples, > >> from terms to terms in one language. > >> > >> Does anyone have a pointer towards something similar? Or insight into > >> which Redex technique might be appropriate? Or a simple two-line email > >> saying it's impossible? :p I have the PLT Redex book, but haven't got > >> the impression my case fits well into one of the many examples. I would > >> be happy to be told otherwise though. > >> > >> I'm sorry for the long-winded email, which probably still leaves details > >> unclear. Don't hesitate to prod me for more details. There is a write-up > >> of this exact system at [1], but it's perhaps a bit long for casual > >> potential helpers to look at. > >> > >> Kind regards, > >> p. > >> > >> 0. < > >> https://groups.google.com/forum/#!searchin/racket-users/redex/racket-users/lKg-77Wh8M0/ULAxOHtENCQJ > >> > > >> 1. <http://people.bordeaux.inria.fr/pwalt/docs/decls.pdf> > >> > >> -- > >> You received this message because you are subscribed to the Google Groups > >> "Racket Users" group. > >> To unsubscribe from this group and stop receiving emails from it, send an > >> email to [email protected]. > >> For more options, visit https://groups.google.com/d/optout. > >> > > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
