Re: Formal methods?

[Atle]

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