[erlang-questions] Looking for tricky protocol examples for verification research
Fri Oct 31 05:47:31 CET 2014
In other words, you want to define a contractual way that different processes
can verify the external behavior of one another, instead of doing the actor
version of duck typing that we tend to use all the time?
If this is a runtime thing (and it would have to be in the case of empty
processes which get assigned their behavior at runtime), then there would have
to be a way to interrogate a process and ask it what messages it listens for
and what the return type (if any) or side effects (if any) of receipt of those
would be. Actually, it wouldn't be hard to write a framework or behavior that
did exactly that. You would, as always, be depending on the programmer to not
forget things and for processes to always tell the truth (consider the games
we play with Dialyzer).
Is this sort of what you are getting at?
On Thursday 30 October 2014 17:43:51 Jonathan Schuster wrote:
> More generally, I'm looking for the kinds of scenarios that one might use
> contracts to specify in a non-concurrent world: instances in which you
> expect some component you're interacting with to have a certain behavior,
> so you specify that behavior in some way that the computer understands. My
> hunch is that something similar could be useful for communication-focused
> programs, but it's unclear what. It would be especially useful if anyone
> points out in these examples "at line X of file Y, I want to state
> invariant Z but have no way of doing so".
> From what I've seen, session types come closest to solving this problem,
> but they tend to be overly restrictive, and it's not obvious how to apply
> session types to actor-based programs, because session types assume that
> channels are created separately from the processes that receive messages on
> I'm especially interested in examples that expect a particular behavior
> from PIDs sent as messages, since this adds an extra layer of complexity
> not normally addressed in the classic communicating finite state machine
> literature. Session types deal with this with what they call "carried
> types", and I'm curious what other mechanisms I might be able to devise for
> those situations.
More information about the erlang-questions