David Welch wrote:
> >
> I don't know about VDM or B, but Z isn't designed to specify concurrent
> programs. How will you handle this?
I am not sure yet, I haven't even tried a 'test' case.
Currenty, I am going through and consolidating what I know so far about how to specify
systems in general, the standard 'hello,
world' version of VDM-SL, specifying fx. List, Stack and Queue as ADT (abstract Data
Type) so that I will feel 'proficient' with
this. Formal methods (mathematical modelling) is really a lot like C, Pentium and PC,
you have to 'play' with it to get a 'feel' for
it.
That is where I am right now.
To tackle concurrency, deterministic and non-deterministic alternation, I am *really*
not sure.
Anyone who knows something about this, please contact me with pointers to information!
I have tentatively specified a 'Semaphore' ADT with two operations, P and V.
The semaphore data itself can be represented by a Set, I described it as S={x} where x
is an integer.
The V operation would the simply return a new set where the value of x is incremented.
The P operation would then contain the actual 'timing' in that it returns a new
semaphore with x decremented, but depending on the
initial value of x, may perform an operation WAIT first.
This captures almost no synchronization semantics whatsoever, except the vague notion
that it either 'waits' or accesses the
semaphore directly.
So I guess it should be considered a kludgus gigantecus non implementabilis ...
But, there is another way:
I have been reading about CSP, which is a great language for modelling concurrency:
A || B is the notation for process A and B running 'interleaved' with no
synchronization, the || operator can be subscripted with an
'alphabet' on which A and B synchronize.
Events are written a->B and the events also can have an alphabet.
One interesting notation is the channel.value with ? and ! meaning in and out,
respectively.
This is *excactly* what is needed. CSP contains everything, except (at least where I
am in the book :-) really good tools for
reification.
So, there may be two ways: Specify top-down in CSP as far as it goes, and then take
over with VDM-SL.
I am on some uncertain terrain here now, but I think I have heard of a concurrency
addition to VDM-SL, that would give the benefit
of staying with one notation all the way.
I am not a big believer in coding C from 'pseudo-code' - so VDM-SL would be the
'coding sheets', unfortunately, I cannot give an
example, because there are some symbols used that are not part of any fonts that I
know of, so I have also had to learn LaTeX in the
process :-)
But it goes something like this:
P:SEM->SEM (P takes a SEM and returns a SEM, it should be specified elsewhere what SEM
is, except where components are manipulated
directly).
p(S)->S' (names the variables used.)
pre-p: S={x} AND x=1 OR x=0 (To take with BIG pinch of salt :-)
post-p: x' IN S' AND x in S AND x=1 AND x'=x-1 OR x=0 AND WAIT (pinch of salt, as
needed )
With the aid of CSP, it would be a lot more elegant:
Processes A and B could have been specified in VDM-SL, so could the CSP channels and
alphabets, but as I say, I am really not sure.
I only got this idea a couple of weeks ago, with Georges Mariano who will do this for
Linux.
What I wanted to know now, is whether or not someone else might be interested in this,
it is a HUGE job, but the benefits are HUGER!
I don't know if it is necessary to mention that IBM sent systems developed this way to
market without testing, and they had fewer
bugs than the thoroughly tested systems!
The 80-20 rule will change: We will spend 80% of the time with the system's logic, and
20% with the bugs, if even that.
If Hurd was completely specified in VDM-SL, it would be the Hurd drivers that would be
ported to Linux, and not the other way
around.
If you are interested in this, it will not be necessary with a lot of mathematical
knowledge, after all, what we will be doing is
simply stating what processes should do ... simple routines (remember, it's only ones
and zeroes :-) that will give us (and) the
implementors better insight in both the system and the ways to implement it...
Best wishes, Atle
_______________________________________________
Help-hurd mailing list
[EMAIL PROTECTED]
http://mail.gnu.org/mailman/listinfo/help-hurd
